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
1k
An Overview of the PureScript Type System
paf31
5
1.9k
Fun with Profunctors
paf31
3
1.3k
Intro to psc-package
paf31
0
150
Stack Safety for Free
paf31
0
320
Other Decks in Programming
See All in Programming
チームの境界をブチ抜いていけ
tokai235
0
180
CSC509 Lecture 06
javiergs
PRO
0
260
バッチ処理を「状態の記録」から「事実の記録」へ
panda728
PRO
0
170
登壇は dynamic! な営みである / speech is dynamic
da1chi
0
340
Swift Concurrency - 状態監視の罠
objectiveaudio
2
540
Range on Rails ―「多重範囲型」という新たな選択肢が、複雑ロジックを劇的にシンプルにしたワケ
rizap_tech
0
6.7k
What's new in Spring Modulith?
olivergierke
1
160
XP, Testing and ninja testing ZOZ5
m_seki
3
700
品質ワークショップをやってみた
nealle
0
530
なぜあの開発者はDevRelに伴走し続けるのか / Why Does That Developer Keep Running Alongside DevRel?
nrslib
3
410
Introduce Hono CLI
yusukebe
6
2.8k
Go Conference 2025: Goで体感するMultipath TCP ― Go 1.24 時代の MPTCP Listener を理解する
takehaya
9
1.7k
Featured
See All Featured
Performance Is Good for Brains [We Love Speed 2024]
tammyeverts
12
1.2k
Rebuilding a faster, lazier Slack
samanthasiow
84
9.2k
Being A Developer After 40
akosma
91
590k
Six Lessons from altMBA
skipperchong
29
4k
Done Done
chrislema
185
16k
The Pragmatic Product Professional
lauravandoore
36
6.9k
KATA
mclloyd
PRO
32
15k
Building a Scalable Design System with Sketch
lauravandoore
463
33k
Code Reviewing Like a Champion
maltzj
526
40k
Side Projects
sachag
455
43k
StorybookのUI Testing Handbookを読んだ
zakiyama
31
6.2k
Practical Tips for Bootstrapping Information Extraction Pipelines
honnibal
PRO
23
1.5k
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