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.7k
Incremental Programming in PureScript
paf31
3
990
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
310
Other Decks in Programming
See All in Programming
ファインディ株式会社におけるMCP活用とサービス開発
starfish719
0
1.5k
知っているようで知らない"rails new"の世界 / The World of "rails new" You Think You Know but Don't
luccafort
PRO
1
160
CloudflareのChat Agent Starter Kitで簡単!AIチャットボット構築
syumai
2
500
AIコーディングAgentとの向き合い方
eycjur
0
270
複雑なフォームに立ち向かう Next.js の技術選定
macchiitaka
2
130
Ruby Parser progress report 2025
yui_knk
1
440
Deep Dive into Kotlin Flow
jmatsu
1
340
go test -json そして testing.T.Attr / Kyoto.go #63
utgwkk
3
300
@Environment(\.keyPath)那么好我不允许你们不知道! / atEnvironment keyPath is so good and you should know it!
lovee
0
120
Testing Trophyは叫ばない
toms74209200
0
880
個人軟體時代
ethanhuang13
0
320
Laravel Boost 超入門
fire_arlo
3
220
Featured
See All Featured
A Modern Web Designer's Workflow
chriscoyier
696
190k
Building a Modern Day E-commerce SEO Strategy
aleyda
43
7.6k
Art, The Web, and Tiny UX
lynnandtonic
303
21k
Into the Great Unknown - MozCon
thekraken
40
2k
Dealing with People You Can't Stand - Big Design 2015
cassininazir
367
27k
実際に使うSQLの書き方 徹底解説 / pgcon21j-tutorial
soudai
PRO
188
55k
Design and Strategy: How to Deal with People Who Don’t "Get" Design
morganepeng
131
19k
We Have a Design System, Now What?
morganepeng
53
7.8k
"I'm Feeling Lucky" - Building Great Search Experiences for Today's Users (#IAC19)
danielanewman
229
22k
Navigating Team Friction
lara
189
15k
The Language of Interfaces
destraynor
161
25k
Stop Working from a Prison Cell
hatefulcrawdad
271
21k
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