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
320
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.6k
Incremental Programming in PureScript
paf31
3
970
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
300
Other Decks in Programming
See All in Programming
Webの外へ飛び出せ NativePHPが切り拓くPHPの未来
takuyakatsusa
2
190
レガシーシステムの機能調査・開発におけるAI利活用
takuya_ohtonari
0
610
「ElixirでIoT!!」のこれまでとこれから
takasehideki
0
370
設計やレビューに悩んでいるPHPerに贈る、クリーンなオブジェクト設計の指針たち
panda_program
3
280
関数型まつりレポート for JuliaTokai #22
antimon2
0
130
なぜ適用するか、移行して理解するClean Architecture 〜構造を超えて設計を継承する〜 / Why Apply, Migrate and Understand Clean Architecture - Inherit Design Beyond Structure
seike460
PRO
1
280
第9回 情シス転職ミートアップ 株式会社IVRy(アイブリー)の紹介
ivry_presentationmaterials
1
200
SODA - FACT BOOK
sodainc
1
1.1k
複数アプリケーションを育てていくための共通化戦略
irof
10
4k
KotlinConf 2025 現地で感じたServer-Side Kotlin
n_takehata
1
220
DroidKnights 2025 - 다양한 스크롤 뷰에서의 영상 재생
gaeun5744
3
300
エンジニア向け採用ピッチ資料
inusan
0
140
Featured
See All Featured
Keith and Marios Guide to Fast Websites
keithpitt
411
22k
Reflections from 52 weeks, 52 projects
jeffersonlam
351
20k
Building Better People: How to give real-time feedback that sticks.
wjessup
367
19k
Embracing the Ebb and Flow
colly
86
4.7k
ReactJS: Keep Simple. Everything can be a component!
pedronauck
667
120k
YesSQL, Process and Tooling at Scale
rocio
173
14k
Designing for humans not robots
tammielis
253
25k
Become a Pro
speakerdeck
PRO
28
5.4k
Site-Speed That Sticks
csswizardry
10
650
The Web Performance Landscape in 2024 [PerfNow 2024]
tammyeverts
8
660
RailsConf 2023
tenderlove
30
1.1k
Building Applications with DynamoDB
mza
95
6.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