Improving Program Quality with Type Enforcement and Error Messages

Slide Note

Microsoft Research's Simon Peyton Jones discussed the importance of rejecting bad programs with clear error messages and accepting well-structured programs. The content also includes a code snippet related to sorting and reversing with type constraints.

kyle_687 Follow

Uploaded on Oct 10, 2024 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

E N D

Presentation Transcript

Simon Peyton Jones Microsoft Research Lambdale Sept 2019

Reject bad programs Accept good programs

Reject bad programs, with a decent error message Accept Elaborate good programs

$fOrdInt comes from instance Ord Int where sort :: reverse :: a. Ord a => [a] -> [a] a. [a] -> [a] foo :: [Int] -> [Int] foo = \xs. sort (reverse xs) $fOrdInt :: Ord Int foo :: [Int] -> [Int] foo = \(xs:[Int]). sort @Int $fOrdInt (reverse @Int xs) Elaboration Decorate every binder with its type Add type applications Add dictionary applications

sort :: reverse :: a. Ord a => [a] -> [a] a. [a] -> [a] foo :: foo = \xs. sort (reverse xs) a. Ord a => [a] -> [a] foo :: foo = /\a. \(d:Ord a). \(xs:a). sort @a d (reverse @a xs) a. Ord a => [a] -> [a] Elaboration Decorate every binder with its type Add type applications and abstractions Add dictionary applications and abstractions

sort :: concat :: a. Ord a => [a] -> [a] a. [[a]] -> [a] foo :: foo = \xs. concat (sort xs) a. Ord a => [[a]] -> [a] $fOrdList :: a. Ord a -> Ord [a] Elaboration Decorate every binder with its type Add type applications and abstractions Add dictionary applications and abstractions, andlocal bindings foo :: foo = /\a. \(d:Ord a). \(xs:a). let d2:Ord [a] d2 = $fOrdList @a d in concat @a (sort @[a] d2 xs) a. Ord a => [a] -> [a] $fOrdList comes from instance Ord a => Ord [a] where

reverse :: and :: [Bool] -> Bool a. [a] -> [a] foo = \xs. (reverse xs, and xs) Start with (xs: ), where is a unification variable, standing for an as-yet-unknown type Typecheck (reverse xs) Instantiate reverse with a unification variable , standing for another as-yet-unknown type. So this occurrence of reverse has type [ ] -> [ ]. Constrain expected arg type [ ] equal to actual arg type , thus ~ [ ].

reverse :: and :: [Bool] -> Bool a. [a] -> [a] foo = \xs. (reverse xs, and xs) Start with (xs: ), where is a unification variable, standing for an as-yet-unknown type Typecheck (reverse xs) Instantiate reverse with a unification variable , standing for another as- yet-unknown type. So this occurrence of reverse has type [ ] -> [ ]. Constrain expected arg type [ ] equal to actual arg type , thus ~ [ ]. Typecheck (and xs) Constrain expected arg type [Bool] equal to actual arg type , thus ~ [Bool]. So we need ( ~ [ ], ~ [Bool]) Solve by unification, yielding a substitution: := [Bool], := Bool

reverse :: and :: [Bool] -> Bool a. [a] -> [a] foo = \(xs: ). (reverse @ xs, and xs) Elaborate foo = \xs. (reverse xs, and xs) Apply the substitution (zonking) Constraints ~ [ ], ~ [Bool] foo = \(xs:[Bool]). (reverse @Bool xs, and xs) Solve, by unification to produce a substitution Main point: solving the constraints fills in the elaborated program := [Bool], := Bool

A unification variable stands for a type; its a type that we don t yet know GHC sometimes calls it a meta type variable By the time type inference is finished, we should know what every meta-tyvar stands for. The global substitution maps each meta-tyvar to the type it stands for. A meta-tyvar stands only for a monotype; a type with no foralls in it.

sort :: reverse :: a. Ord a => [a] -> [a] a. [a] -> [a] foo = \(xs:[Int]). sort @ d (reverse @ xs) Elaborate foo :: [Int] -> [Int] foo = \xs. sort (reverse xs) Constraints Apply the substitution [ ] ~ [ ], [ ] ~ [Int], d:Ord foo = \(xs:[Int]). sort @Int $fOrdInt (reverse @Int xs) Solve, by unification := Int, := Int, d := $fOrdInt Main point: solving the constraints fills in the elaborated program

Main point Old school: on the fly solving Encounter a unification problem Solve it If fails, report error Otherwise, proceed This will not work any more The order in which we encounter constraints The order in which we solve them [ ] ~ [ ], [ ] ~ [Int], d:Ord We have to solve := Int, before we can solve d:Ord

x:: Instantiate g at g :: F a -> a -> Int type instance F Bool = Bool f x = (g True x, ...., not x) g True F ~ Bool, ~ , ~ Bool Order of encounter g True x not x We have to solve this first

op :: C a x => a -> x -> Int instance Eq a => C a Bool f x = let g :: a Eq a => a -> a g a = op a x in g (not x) x : Constraint: C a Cannot solve constraint (C a ) until we later discover that ( ~ Bool) Again, need to defer constraint solving, rather than doing it all on the fly

Elaborated source program Haskell source program Apply Elaborated program with holes substitution Constraint generation Large Constraints syntax, with many many constructors Substitution Small syntax, with few constructors Solve Residual constraint Report errors The essence of ML type inference, Pottier & Remy, In ATAPL, Pierce, 2005.

Haskell source program What exactly is this? Constraints Constraint generation Small syntax, with few constructors Large syntax, with many many constructors How does solving work? Solve Residual constraint Report errors

W ::= ? | W1 , W2 | C 1.. n | 1 ~ 2 | a1..an. W1 Empty constraint Conjunction Class constraint Equality constraint W2Implication

W ::= ? | W1 , W2 | d : C 1.. n | g : 1 ~ 2 | a1..an. W1 Empty constraint Conjunction Class constraint Equality constraint W2Implication Evidence

[] ~ [], [] ~ [Int], d:Ord Decompose ? ~ [?] ~ , [ ] ~ [Int], d:Ord 1. 2. Do one rewrite 3. Repeat from 1 Take the constraints Substitute ? ? [ ] ~ [Int], d:Ord ? ? ? Decompose ? ~ [???] ~ Int, d:Ord ? Each step takes a set of constraints and returns a logically-equivalent set of constraints. When you can t do any more, that s the residual constraint Substitute ? ??? ? ? ??? d:Ord ??? Solve ?:??? ??? from instance declaration ?

Constraint solving takes place by successive rewrites of the constraint Each rewrite generates a binding, for a type variable (fixing a unification variable) a dictionary (class constraints) a coercion (equality constraint) as we go Bindings record the proof steps Bindings get injected back into the term

data T where MkT :: a. Show a => a -> T ts = [ MkT @Int $fShowInt 3 , MkT @Bool $fShowBool True ] ts :: [T] ts = [MkT 3, MkT True]

MkT :: a. Show a => a -> T show :: a. Show a => a -> String ts :: [T] ts = [MkT 3, MkT True] ts = [ MkT @Int $fShowInt 3 , MkT @Bool $fShowBool True ] f = \(t:T). case t of MkT a (gd:Show a) (x:a) -> show @a gd x f :: T -> String f = \t. case t of MkT x -> show x

MkT :: a. Show a => a -> T show :: a. Show a => a -> String f : ? t : ? x : a Instantiate show with ? f = \t. case t of { MkT x -> show x } Generate constraints From the lambda From the case ? ~ ? ? ? ~ ? d : Show ? From call of show ? ~ ? From (show x) ? ~ ?????? From result of foo

MkT :: a. Show a => a -> T show :: a. Show a => a -> String f = \t. case t of { MkT x -> show x } Generate constraints But what is this a ? From the lambda From the case ? ~ ? ? ? ~ ? d : Show ? From call of show ? ~ ? From (show x) ? ~ ?????? From result of foo And how can we solve Show ??

f = \t. case t of { MkT x -> show x } Generate constraints MkT :: a. Show a => a -> T show :: a. Show a => a -> String From the lambda From the case But what is this a ? Answer: Bound by ? And how can we solve d : Show ? Answer: from gd. ? ~ ? ? ? ~ ? ?.(?? ???? ?) { ? ? ?? ? , ? ~ ? ,? ~ ?????? } From call of show From (show x) From result of foo

W ::= ? | W1 , W2 | d : C 1.. n | g : 1 ~ 2 | a1..an. W1 Empty constraint Conjunction Class constraint Equality constraint W2Implication Implication constraint Given Wanted

From the lambda From the case ? ~ ? ? ? ~ ? ?.(?? ???? ?) { ? ? ?? ?, ? ~ ?,? ~ ?????? } ?.(?? ???? ?) { ? ? ?? ? , ? ~ ? ,? ~ ?????? } Substitute ? ? From call of show From (show x) From result of foo ?.(?? ???? ?) { ? ? ?? ?, ? ~ ?????? } Solve (d:Show a), substitute d:=gd ? ? ?. ?? ???? ? ? ~ ?????? Solving Substitute ? ?????? ? Elaborated program with holes Elaborated program after filling holes f = \(t: ). case t of MkT a (gd:Show a) (x:a) -> show @ d x f = \(t:T). case t of MkT a (gd:Show a) (x:a) -> show @a gd x

f = \(t:T). case t of MkT a (gd:Show a) (x:a) -> show @a gd x f = \t. case t of MkT x -> show x Generate constraints ? is a unification variable, standing for an as-yet-unknown type. Constraint solving produces a substitution for the unification variables When typechecking is done, all unification variables are gone (substituted away) ? is a skolem constant, the type variable ? bound by the MkT pattern match in the elaborated program. Each pattern match on MkT binds a fresh, distinct a . Every skolem in the constraints should be bound by a ? ~ ? ? ? ~ ? ?.(?? ???? ?) { ? ? ?? ? , ? ~ ? ,? ~ ?????? }

f2 = \t. case t of { MkT x -> x } -- Ill-typed Generate constraints MkT :: a. Show a => a -> T From the lambda From the case ? ~ ? ? ? ~ ? Can we solve by substituting ? ?? ?.(?? ???? ?) { ? ~ ? } From result of foo

f2 = \t. case t of { MkT x -> x } -- Ill-typed Generate constraints MkT :: a. Show a => a -> T From the lambda From the case ? ~ ? ? ? ~ ? Can we solve by substituting ? ?? ?.(?? ???? ?) { ? ~ ? } From result of foo No! No! Noooo! ? comes from an outer scope

f2 = \t. case t of { MkT x -> x } -- Ill-typed Generate constraints Every unification variable has a level number Every implication has a level number We say ?1 is untouchable under the 2 The untouchability rule: you cannot solve ??~?? under a ?, if n<k From the lambda From the case ?1 ~ ?1 ?1 ?1 ~ ? ??.(?? ???? ?) { ?1 ~ ? } From result of foo

f = \t. case t of MkT x -> show x Now what???? Generate constraints ??.(?? ???? ?) { ?1 ~ ?????? } ?1 ~ ?1 ?1 ?1 ~ ? ??.(?? ???? ?) { ? ? ?? ?2 , ?2 ~ ? ,?1 ~ ?????? } ? ? ?1 ? ? ? ? ? is untouchable!

?1 ~ ?????? ??.(?? ???? ?) { ?1 ~ ??????, ? } ??. ?? ???? ? { ? } Float (?1 ~ ??????) outside the Now ?1 is not untouchable any more So we can substitute ?1 ??????

f2 = \t. case t of { MkT x -> x } -- Ill-typed Generate constraints Cannot float ?1 ~ ? outside the ?, obviously, because it mentions ?! From the lambda From the case ?1 ~ ?1 ?1 ?1 ~ ? ??.(?? ???? ?) { ?1 ~ ? } From result of foo

2?. ?1~ (?2 Int),? Can we float this to? ?1~ (?2 Int) 2?. ?

When floating an equality, promote all its free unification variables 2?. ?1~ (?2 Int),? NO! Can we float this to? ?1~ (?2 Int) 2?. ? Instead promote ?2 ?1, so we get ?1~ (?1 Int) 2?. ?

Ever unification variable and implication constraint has a level Unification variable ?? is untouchable under a ? if ? < ? Float an equality (?~?) out of an implication ?.??? , if ? does not appear free in ? or ?. When floating out, promote the free unification variables of the floated constraint F ::= d : C 1.. n | g : 1 ~ 2 | F1 , F2 | True W ::= F | W1 , W2 | k a1..an. F W

When generating constraints for a term, the generator has an ambient level Fresh unification variables are born at this level At a pattern match e.g. case x of { K x y -> rhs } Increment the ambient level Generate constraints for the rhs Wrap them in an implication constraint binding the existentials and constraints of K No need for this wrapping if no existentials or constraints e.g. case x of { Just y -> rhs; }

reverse :: a. [a] -> [a] sort :: a. Ord a => [a] -> [a] f :: a. Ord a => [a] -> [a] f = \xs -> reverse (sort xs) Type signature gives rise to an implication constraint Constraints of the signature become givens of the implication Increment the ambient level before generating constraints for the RHS xs : [?] Instantiate reverse with ? Instantiate sort with ? ??.(?? ??? ?) { ? ??? ?1 , ?1~ [?1] , ?1~ ? } From call of sort Result of sort From result of foo

op :: C a x => a -> x -> Int instance Eq a => C a Bool f x = let g :: a Eq a => a -> a g a = op a x in g (not x) x : Constraint: C a And then this 2?.?? ? ? ? ?1 ?1~ ???? Solve this first

Perform repeated rewrites on the constraints Each rewrite preserves logical meaning Each rewrite is recorded by adding an evidence binding, in the elaborated program The constraint language is very small But solving is quite subtle F ::= d : C 1.. n | g : 1 ~ 2 | F1 , F2 | True W ::= F | W1 , W2 | k a1..an. F W