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
240
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.4k
Incremental Programming in PureScript
paf31
3
910
An Overview of the PureScript Type System
paf31
5
1.8k
Fun with Profunctors
paf31
3
990
Intro to psc-package
paf31
0
110
Stack Safety for Free
paf31
0
240
Other Decks in Programming
See All in Programming
Jakarta EE meets AI
ivargrimstad
0
390
Kotlin 2.0が与えるAndroid開発の進化
masayukisuda
1
420
Rubyとクリエイティブコーディングの輪の広がり / The Growing Circle of Ruby and Creative Coding
chobishiba
1
270
GraphQLとGigaViewer for Apps
numeroanddev
2
180
Evolution of real-time – Irina Nazarova, EuRuKo, 2024
irinanazarova
0
130
意外とフォントが大事だった話 / Font Issues on Internationalization
fumi23
0
110
LangChainでWebサイトの内容取得やGitHubソースコード取得
shukob
0
160
Understand the mechanism! Let's do screenshots tests of Compose Previews with various variations / 仕組みから理解する!Composeプレビューを様々なバリエーションでスクリーンショットテストしよう
sumio
3
870
Ruby Parser progress report 2024
yui_knk
2
230
Boost Performance and Developer Productivity with Jakarta EE 11
ivargrimstad
0
530
開発を加速する共有Swift Package実践
elmetal
PRO
0
420
Modern Angular with the NGRX Signal Store New Rules for Your Architecture @BASTA! 2024 in Mainz
manfredsteyer
PRO
0
160
Featured
See All Featured
Atom: Resistance is Futile
akmur
261
25k
Agile that works and the tools we love
rasmusluckow
327
20k
Navigating Team Friction
lara
183
13k
Speed Design
sergeychernyshev
22
430
The Cult of Friendly URLs
andyhume
76
6k
Automating Front-end Workflow
addyosmani
1365
200k
Building an army of robots
kneath
302
42k
Let's Do A Bunch of Simple Stuff to Make Websites Faster
chriscoyier
502
140k
How to name files
jennybc
75
98k
Robots, Beer and Maslow
schacon
PRO
157
8.2k
Gamification - CAS2011
davidbonilla
79
5k
What the flash - Photography Introduction
edds
67
11k
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