Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
Principal type-schemes for functional programs
Search
Phil Freeman
June 28, 2017
Programming
0
340
Principal type-schemes for functional programs
Phil Freeman
June 28, 2017
Tweet
Share
More Decks by Phil Freeman
See All by Phil Freeman
The Future Is Comonadic!
paf31
14
4.7k
Incremental Programming in PureScript
paf31
3
990
An Overview of the PureScript Type System
paf31
5
1.9k
Fun with Profunctors
paf31
3
1.2k
Intro to psc-package
paf31
0
150
Stack Safety for Free
paf31
0
310
Other Decks in Programming
See All in Programming
プログラミングどうやる? ~テスト駆動開発から学ぶ達人の型~
a_okui
0
190
iOSエンジニア向けの英語学習アプリを作る!
yukawashouhei
0
170
あなたの知らない「動画広告」の世界 - iOSDC Japan 2025
ukitaka
0
340
なぜGoのジェネリクスはこの形なのか? Featherweight Goが明かす設計の核心
ryotaros
7
1k
(Extension DC 2025) Actor境界を越える技術
teamhimeh
1
200
そのpreloadは必要?見過ごされたpreloadが技術的負債として爆発した日
mugitti9
2
2.8k
私はどうやって技術力を上げたのか
yusukebe
43
17k
CSC509 Lecture 02
javiergs
PRO
0
400
Reduxモダナイズ 〜コードのモダン化を通して、将来のライブラリ移行に備える〜
pvcresin
2
670
CSC305 Lecture 04
javiergs
PRO
0
230
Swiftビルド弾丸ツアー - Swift Buildが作る新しいエコシステム
giginet
PRO
0
1.6k
GraphQL×Railsアプリのデータベース負荷分散 - 月間3,000万人利用サービスを無停止で
koxya
1
1k
Featured
See All Featured
jQuery: Nuts, Bolts and Bling
dougneiner
64
7.9k
Design and Strategy: How to Deal with People Who Don’t "Get" Design
morganepeng
132
19k
Embracing the Ebb and Flow
colly
88
4.8k
Understanding Cognitive Biases in Performance Measurement
bluesmoon
29
2.6k
The Cost Of JavaScript in 2023
addyosmani
53
9k
Documentation Writing (for coders)
carmenintech
75
5k
Visualizing Your Data: Incorporating Mongo into Loggly Infrastructure
mongodb
48
9.7k
Unsuck your backbone
ammeep
671
58k
Let's Do A Bunch of Simple Stuff to Make Websites Faster
chriscoyier
507
140k
Building a Scalable Design System with Sketch
lauravandoore
462
33k
Fireside Chat
paigeccino
40
3.7k
Cheating the UX When There Is Nothing More to Optimize - PixelPioneers
stephaniewalter
285
14k
Transcript
Principal type-schemes for functional programs Luis Damas and Robin Milner
(POPL `82)
Agenda • Slides • Code
ML • Meta Language for LCF • Type inference •
Influence on Haskell, Rust, F#, OCaml, ... • “Sweet spot” in type system design
ML letrec f xs = if null xs then nil
else snoc (f (tl xs)) (hd xs) What type does this function have? null : ∀ ( list → bool) snoc : ∀ ( list → → list) hd, tl : ∀ ( list → ) nil : ∀ ( list)
ML What about: let s x y z = x
z (y z) ?
Type Inference f : ∀ ( list → list) •
Given f, how can we infer this type? • What does it even mean for a value to have a type? • How can we be sure we have the most general type?
Lambda Calculus Expressions e: • Identifiers: , , … •
Applications: e e’ • Abstractions: . e • Let bindings: let = e in e’
Lambda Calculus For example: . . . . let =
. . in
Types Monotypes : • Variables: • Primitives: • Functions: →
Type Schemes Type schemes : • Monomorphic: • Polymorphic: ∀
. Type schemes are types with identifiers bound by ∀ at the front.
Substitutions Mappings from variables to types • Can instantiate type
schemes using substitutions • Gives a simple subtyping relation on type schemes
Semantics Construct a semantic domain (CPO) V containing • Primitives
• Functions • An error element and a semantic function : e → (Id → V) → V
Semantics Identify types with subsets of V Define the judgment
A ╞ e : when (∀ ( : ’) ∈ A. ∈ ’) ⇒ e ∈
Declarative System Variable rule:
Declarative System Application rule:
Declarative System Abstraction rule:
Declarative System Let rule:
Declarative System Instantiation rule:
Declarative System Generalization rule:
Soundness If A e : then A ╞ e :
“Static behavior determines dynamic behavior”
Example Prove: . : ∀ . ( → → )
→ →
Algorithm W • The inference rules do not translate easily
into an algorithm (why not?) • Introduce w : Exp → Env → (Env, )
Algorithm W • W attempts to build a substitution, bottom-up
• W can fail with an error if there is no valid typing • Intuition: ◦ Collect constraints ◦ Then solve constraints • Reality: W is the fusion of these two steps • See the code!
Unification • Unification gives local information about types • We
assemble a global solution from local information
Unification Example: ( → ) ~ (( → ) →
) ~ ( → ) ~ ~ ( → )
Occurs Check Prevents inference of infinite types w( . ,
nil) = error! Can’t unify ~ if occurs in the body of . E.g. ~ → ~ ((… → ) → ) →
Soundness If w(A, e) = (S, ) then A e
: “Algorithm W constructs typing judgments”
Completeness If A e : then w(A, e) constructs a
typing judgment for e which generalises the above. “Algorithm W constructs principal types”
Further Reading More type systems • System F, F⍵ •
Rank-N types • Type Classes • Dependent Types • Refinement Types Other approaches • Constraints • Bidirectional typechecking • SMT See TAPL & ATAPL!
Acknowledgments DHM axioms reproduced from Wikipedia under the CC-3.0 Attribution/ShareAlike
license