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
140
Stack Safety for Free
paf31
0
300
Other Decks in Programming
See All in Programming
rbs-traceを使ってWEARで型生成を試してみた After RubyKaigi 2025〜ZOZO、ファインディ、ピクシブ〜 / tried rbs-trace on WEAR
oyamakei
0
1.1k
Devinで実践する!AIエージェントと協働する開発組織の作り方
masahiro_nishimi
6
2.5k
TVer iOSチームの共通認識の作り方 - Findy Job LT iOSアプリ開発の裏側 開発組織が向き合う課題とこれから
techtver
PRO
0
710
OpenNext + Hono on Cloudflare でイマドキWeb開発スタックを実現する
rokuosan
0
110
try-catchを使わないエラーハンドリング!? PHPでResult型の考え方を取り入れてみよう
kajitack
3
310
ワンバイナリWebサービスのススメ
mackee
10
7.5k
MLOps Japan 勉強会 #52 - 特徴量を言語を越えて一貫して管理する, 『特徴量ドリブン』な MLOps の実現への試み
taniiicom
2
570
DevTalks 25 - Create your own AI-infused Java apps with ease
kdubois
2
120
❄️ tmux-nixの実装を通して学ぶNixOSモジュール
momeemt
1
120
テスト分析入門/Test Analysis Tutorial
goyoki
11
2.7k
メモリリークが発生した時にpprofを使用して原因特定した話
zono33lhd
0
100
Proxmoxをまとめて管理できるコンソール作ってみました
karugamo
1
410
Featured
See All Featured
Embracing the Ebb and Flow
colly
85
4.7k
Learning to Love Humans: Emotional Interface Design
aarron
273
40k
I Don’t Have Time: Getting Over the Fear to Launch Your Podcast
jcasabona
32
2.3k
Building Adaptive Systems
keathley
41
2.6k
Put a Button on it: Removing Barriers to Going Fast.
kastner
60
3.9k
How STYLIGHT went responsive
nonsquared
100
5.6k
RailsConf 2023
tenderlove
30
1.1k
[Rails World 2023 - Day 1 Closing Keynote] - The Magic of Rails
eileencodes
34
2.3k
ReactJS: Keep Simple. Everything can be a component!
pedronauck
667
120k
YesSQL, Process and Tooling at Scale
rocio
172
14k
Save Time (by Creating Custom Rails Generators)
garrettdimon
PRO
31
1.2k
The Power of CSS Pseudo Elements
geoffreycrofte
76
5.8k
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