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
330
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
980
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
AI駆動のマルチエージェントによる業務フロー自動化の設計と実践
h_okkah
0
230
DMMを支える決済基盤の技術的負債にどう立ち向かうか / Addressing Technical Debt in Payment Infrastructure
yoshiyoshifujii
3
410
AI時代のソフトウェア開発を考える(2025/07版) / Agentic Software Engineering Findy 2025-07 Edition
twada
PRO
99
37k
“いい感じ“な定量評価を求めて - Four Keysとアウトカムの間の探求 -
nealle
2
12k
NEWT Backend Evolution
xpromx
1
140
React は次の10年を生き残れるか:3つのトレンドから考える
oukayuka
7
2.4k
RailsGirls IZUMO スポンサーLT
16bitidol
0
200
フロントエンドのパフォーマンスチューニング
koukimiura
5
2k
Claude Code派?Gemini CLI派? みんなで比較LT会!_20250716
junholee
1
530
チームのテスト力を総合的に鍛えて品質、スピード、レジリエンスを共立させる/Testing approach that improves quality, speed, and resilience
goyoki
5
1.1k
Android 16KBページサイズ対応をはじめからていねいに
mine2424
0
440
AIともっと楽するE2Eテスト
myohei
8
3k
Featured
See All Featured
Designing Experiences People Love
moore
142
24k
Chrome DevTools: State of the Union 2024 - Debugging React & Beyond
addyosmani
7
750
Imperfection Machines: The Place of Print at Facebook
scottboms
267
13k
Exploring the Power of Turbo Streams & Action Cable | RailsConf2023
kevinliebholz
34
5.9k
Building Better People: How to give real-time feedback that sticks.
wjessup
367
19k
Why You Should Never Use an ORM
jnunemaker
PRO
58
9.5k
Large-scale JavaScript Application Architecture
addyosmani
512
110k
Responsive Adventures: Dirty Tricks From The Dark Corners of Front-End
smashingmag
251
21k
Writing Fast Ruby
sferik
628
62k
The Art of Programming - Codeland 2020
erikaheidi
54
13k
No one is an island. Learnings from fostering a developers community.
thoeni
21
3.4k
The Cost Of JavaScript in 2023
addyosmani
51
8.6k
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