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
260
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
920
An Overview of the PureScript Type System
paf31
5
1.8k
Fun with Profunctors
paf31
3
1k
Intro to psc-package
paf31
0
120
Stack Safety for Free
paf31
0
250
Other Decks in Programming
See All in Programming
Pinia Colada が実現するスマートな非同期処理
naokihaba
4
230
リアーキテクチャxDDD 1年間の取り組みと進化
hsawaji
1
220
Jakarta EE meets AI
ivargrimstad
0
670
カンファレンスの「アレ」Webでなんとかしませんか? / Conference “thing” Why don't you do something about it on the Web?
dero1to
1
100
Compose 1.7のTextFieldはPOBox Plusで日本語変換できない
tomoya0x00
0
190
役立つログに取り組もう
irof
28
9.6k
Snowflake x dbtで作るセキュアでアジャイルなデータ基盤
tsoshiro
2
520
受け取る人から提供する人になるということ
little_rubyist
0
250
Make Impossible States Impossibleを 意識してReactのPropsを設計しよう
ikumatadokoro
0
240
flutterkaigi_2024.pdf
kyoheig3
0
150
Laravel や Symfony で手っ取り早く OpenAPI のドキュメントを作成する
azuki
2
120
よくできたテンプレート言語として TypeScript + JSX を利用する試み / Using TypeScript + JSX outside of Web Frontend #TSKaigiKansai
izumin5210
6
1.7k
Featured
See All Featured
Product Roadmaps are Hard
iamctodd
PRO
49
11k
Practical Orchestrator
shlominoach
186
10k
Making Projects Easy
brettharned
115
5.9k
Documentation Writing (for coders)
carmenintech
65
4.4k
Building Better People: How to give real-time feedback that sticks.
wjessup
364
19k
How to train your dragon (web standard)
notwaldorf
88
5.7k
Building Your Own Lightsaber
phodgson
103
6.1k
Principles of Awesome APIs and How to Build Them.
keavy
126
17k
Docker and Python
trallard
40
3.1k
The Pragmatic Product Professional
lauravandoore
31
6.3k
[Rails World 2023 - Day 1 Closing Keynote] - The Magic of Rails
eileencodes
33
1.9k
Designing Dashboards & Data Visualisations in Web Apps
destraynor
229
52k
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