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
250
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
910
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
Server Driven Compose With Firebase
skydoves
0
400
Sidekiqで実現する 長時間非同期処理の中断と再開 / Pausing and Resuming Long-Running Asynchronous Jobs with Sidekiq
hypermkt
6
2.7k
カラム追加で増えるActiveRecordのメモリサイズ イメージできますか?
asayamakk
4
1.5k
Kaigi on Rails 2024 - Rails APIモードのためのシンプルで効果的なCSRF対策 / kaigionrails-2024-csrf
corocn
5
3.3k
推し活の ハイトラフィックに立ち向かう Railsとアーキテクチャ - Kaigi on Rails 2024
falcon8823
6
2.1k
のびしろを広げる巻き込まれ力:偶然を活かすキャリアの作り方/oso2024
takahashiikki
1
410
Nuxtベースの「WXT」でChrome拡張を作成する | Vue Fes 2024 ランチセッション
moshi1121
1
500
PHP でアセンブリ言語のように書く技術
memory1994
PRO
1
150
LLM生成文章の精度評価自動化とプロンプトチューニングの効率化について
layerx
PRO
2
130
Kotlin2でdataクラスの copyメソッドを禁止する/Data class copy function to have the same visibility as constructor
eichisanden
1
130
Amazon Neptuneで始めてみるグラフDB-OpenSearchによるグラフの全文検索-
satoshi256kbyte
4
320
【Kaigi on Rails 2024】YOUTRUST スポンサーLT
krpk1900
1
240
Featured
See All Featured
Creating an realtime collaboration tool: Agile Flush - .NET Oxford
marcduiker
25
1.8k
JavaScript: Past, Present, and Future - NDC Porto 2020
reverentgeek
47
5k
Principles of Awesome APIs and How to Build Them.
keavy
126
17k
[RailsConf 2023 Opening Keynote] The Magic of Rails
eileencodes
28
9.1k
Fight the Zombie Pattern Library - RWD Summit 2016
marcelosomers
231
17k
Ruby is Unlike a Banana
tanoku
96
11k
Keith and Marios Guide to Fast Websites
keithpitt
408
22k
Faster Mobile Websites
deanohume
304
30k
Responsive Adventures: Dirty Tricks From The Dark Corners of Front-End
smashingmag
250
21k
4 Signs Your Business is Dying
shpigford
180
21k
Practical Tips for Bootstrapping Information Extraction Pipelines
honnibal
PRO
9
680
The Success of Rails: Ensuring Growth for the Next 100 Years
eileencodes
43
6.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