=========================[ Readings ]============================== Read Chapter 6 of the textbook. Focus on Section 6.3, "Type Inference". Depending on your learning style, you may find the following sources helpful to understand the Hindley-Milner-Damas type inference algorithm: https://slightknack.dev/passerine/type-inference/ -- Cornell lecture notes, gives examples of type reference in OCaml. OCaml's syntax is slightly different, "let g = fun x -> ((+) 5) x" would be "let g = \ x -> ((+) 5) x" in Haskell and type variables are written 'a, 'b, etc. OCaml has more "fun" :) https://bernsteinbear.com/blog/type-inference/ -- explanations of inference algorithms with Python implementations ------------[ Getting systematic the way PL papers do ]------------ For a systematic mathematical discussion of ML's, Haskell's, OCaml's underlying type system see "The Hindley-Milner Type Inference Algorithm", Ian Grant, 2011, https://steshaw.org/hm/hindley-milner.pdf In class, we looked at p.5 of that paper for the definition of the simply-typed lambda calculus, in the sequent notation (assumptions above the line, derivations from these assumptions under the line). Check that these rules make the most intuitive and trivial sense, e.g., if some expression E' can be derived to have type t' and another expression E---typically constructed as a lambda function---can be derived to have type t' -> t, then the application of E to E' will make type t. For short, if we can assume E':t' and E:t'->t then (E E'):t [*]. [*] Compare this with the Boolean logic's inference rule, if A is true and A=>B then B is true, a.k.a. Modus Ponens. The similarity is not coincidental: it connects logic and type theory. Note how these simple definitions, based on nothing other than having primitive type names and the -> constructor to express the idea of a function taking values of some type A to some other type B, A -> B, are already enough to assert that typing is not compatible with potentially endless recursion such as the Y combinator (p.6). For now, skip the discussion of the issues with the "raising" and "lowering" types with Church's integer encoding. On p.11 (Section 7) note the formalization of the Hindley-Milner type system, which adds _parametrized_ types to simple types, with ∀ playing just about the same role for types that λ plays in λ-functions of lambda calculus for expressions. Take a careful look at these rules, and see that they are similarly intuitive as those for simple types on p.6. Note that typed recursion is now possible, see p.8. ----------------------[ More mathematical foundations ]------------------ For a deeper dive into the mathematics of type systems, see "Introduction to generalized type systems", Barendregt, 1991: https://repository.ubn.ru.nl/bitstream/handle/2066/17240/13256.pdf It introduces the famous Lambda Cube of the progressively more complex type systems. Classic papers by Hindley, Milner, and Damas: https://courses.cs.washington.edu/courses/cse503/10wi/readings/p207-damas.pdf https://www.ams.org/journals/tran/1969-146-00/S0002-9947-1969-0253905-6/S0002-9947-1969-0253905-6.pdf https://www.pure.ed.ac.uk/ws/portalfiles/portal/15143545/1_s2.0_0022000078900144_main.pdf ----------------------[ Lists and Nums examples ]---------------------- Use :i and :t in GHCI to check the types of things and get syntax hints on infix operator precedence. For example, the list data constructor (:) is at 5, (+) is at 6. ghci> :i (:) type List :: * -> * data List a = ... | a : [a] -- Defined in ‘GHC.Types’ infixr 5 : ghci> :t (+) (+) :: Num a => a -> a -> a ghci> :i (+) type Num :: * -> Constraint class Num a where (+) :: a -> a -> a ... -- Defined in ‘GHC.Internal.Num’ infixl 6 + So (+) binds stronger, 1+2:[] needs no parens: ghci> 1+2 : [] [3] ghci> (1+2) : [] [3] Remember that (:) and [] are the only two data constructors that make up a list. Everything else, including syntax like [1,2,3] is syntactic sugar. [1,2,3] is literally 1:(2:(3:[])), or, more precisely, "(:) 1 ((:) 2 ((:) 3 []))" if we ditch the infix notation. ghci> [1,2,3] [1,2,3] ghci> 1 : ( 2 : (3 : [])) [1,2,3] ghci> (:) 1 ((:) 2 ((:) 3 [])) [1,2,3] // Note the type of "(:) 1" -- it's a function. What does it work on and what does it do, // in conventional terms? ghci> :t (:) 1 (:) 1 :: Num a => [a] -> [a] // Looking up [] hints at a lot of polymorphic code you will get for free, // and working correctly for your type, i.e., "polymorphically", without // any explicit type annotations: ghci> :i [] type List :: * -> * data List a = [] | a : [a] -- Defined in ‘GHC.Types’ instance Monoid [a] -- Defined in ‘GHC.Internal.Base’ instance Semigroup [a] -- Defined in ‘GHC.Internal.Base’ instance Foldable [] -- Defined in ‘GHC.Internal.Data.Foldable’ instance Traversable [] -- Defined in ‘GHC.Internal.Data.Traversable’ instance Read a => Read [a] -- Defined in ‘GHC.Internal.Read’ instance Eq a => Eq [a] -- Defined in ‘GHC.Classes’ instance Ord a => Ord [a] -- Defined in ‘GHC.Classes’ instance Show a => Show [a] -- Defined in ‘GHC.Internal.Show’ instance Applicative [] -- Defined in ‘GHC.Internal.Base’ instance Functor [] -- Defined in ‘GHC.Internal.Base’ instance MonadFail [] -- Defined in ‘GHC.Internal.Control.Monad.Fail’ instance Monad [] -- Defined in ‘GHC.Internal.Base’ // Since lists are nothing but things build with constructors (:) and [], our length // function only needs to pattern-match on these two constructors: ghci> let mlen [] = 0 ghci| mlen x:xs = 1 + mlen xs -- oops, forgot the parens. I didn't mean (mlen x):xs = .. ! :75:5: error: [GHC-07626] Parse error in pattern: mlen ghci> let mlen [] = 0 ghci| mlen (x:xs) = 1 + mlen xs ghci> :t mlen mlen :: Num t => [a] -> t ghci> mlen [] 0 ghci> mlen ['a','b','c'] -----+---- polymorphism! 3 / ghci> mlen [4,5,6] ---/ 3 / ghci> :t ['a','b','c'] / ['a','b','c'] :: [Char] __/ | ghci> :t [4,5,6] | [4,5,6] :: Num a => [a] __| // This also works for an endlessly repeated series, thanks to Haskell's laziness: ghci> let repeat x = x : repeat x ghci> take 10 (repeat 5) [5,5,5,5,5,5,5,5,5,5] ghci> take 1000 (repeat 5) [5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5,5..,5] // Just in case you wonder what take might do, here is mine: ghci> let mtake 0 _ = [] ghci| mtake n (x:xs) = x : mtake (n-1) xs ghci| ghci> mtake 0 [1,2,3] [] ghci> mtake 2 [1,2,3] [1,2] ghci> mtake 3 [1,2,3] [1,2,3] // Turns out I have a bug. Fix it! Note that Haskell doesn't catch it statically, although one // could imagine that it could. ghci> mtake 4 [1,2,3] [1,2,3*** Exception: :(156,6)-(157,40): Non-exhaustive patterns in function mtake // Idris https://www.idris-lang.org/ and Agda [*] would have the power to catch it. // [*] https://agda.readthedocs.io/en/v2.6.0.1/getting-started/what-is-agda.html // BTW, this is what happened when I forgot the arity of repeat: ghci> let repeat x = x : repeat ghci| :72:5: error: [GHC-83865] • Couldn't match expected type: [a] <<---- See writeup below with actual type: a -> [a] <<---- on how to read this! • Relevant bindings include repeat :: [a] (bound at :72:5) ---------------------------[ GHC errors ]---------------------- A very useful writeup on GHC's type errors. Read pages 2--3, especially the safeHead example: https://jstolarek.github.io/files/stolarek_understanding_basic_haskell_error_messages.pdf ==================[ The Maybe Monad: pipelines aware of exceptional values ]=========== // A pipeline of an automatically constructed type that is a _disjoint union_ of an integer and // a special value Nothing that represents a failure (think NaN for arithmetic). // As motivation, think about the MaxMind bug/feature in their IP address geolocation APIs // which could not handle the special "I don't really know" outcomes, mostly likely because // it was designed to take an IP address and return coordinates: // // https://www.theguardian.com/technology/2016/aug/09/maxmind-mapping-lawsuit-kansas-farm-ip-address // Imagine a type that packages an integer for normal processing and an exceptional NaN. // For all operations in the processing pipeline, NaN sails right through producing another NaN, // whereas integers get arithmetic done to them and handed to the next stage, and so on. // In C, we'd create a struct with an integer and a special flag for "this is a NaN" vs "this is an int", // the trick known as a C tagged union type, and start every function with if(tag==NaN) return NaN; // and then gets the int from the struct, operates on it, and sticks it back into the struct to pass // it on. However, that's a lot of boilerplate code to add. // Instead, we are going to get all that code for free, by using the "Maybe" type. It has // two data contructors, Nothing and Just. Recall that (:) and [] are data contructors for List. // More properly the type is "Maybe a", the constructors are Nothing and "Just a". You can think // of them as creating the tagged C struct somewhere under the hood: Nothing makes an instance // representing a NaN with "I am a NaN" and "Just 5" makes one with the integer 5 and "I am an int" tag. // Now enter >>= , which makes the pipeline, by chaining functions that take an int, do arithmetic // on it and create a tagged struct with the result: ghci> :t >>= type Monad :: (* -> *) -> Constraint class Applicative m => Monad m where (>>=) :: m a -> (a -> m b) -> m b ... -- Defined in ‘GHC.Internal.Base’ infixl 1 >>= <<--- note lowest precedence! ghci> Just 5 >>= \ x -> Just (x*x) >>= \ x -> Just ( x + 1 ) >>= \ y -> Just ( 2*y ) Just 52 // Same thing with unnecessary parens. These >>= do look like piping for the pipeline. ghci> Just 5 >>= (\x->Just(x*x)) >>= (\x->Just(x+1)) >>= (\y->Just(2*y)) Just 52 // Check yourself: do you see left association for >>= ? The first application will be // Just 5 >>= (\x->Just(x*x)) // then (Just 25) >>= (\x->Just(x+1)) // and then (Just 26) >>= (\y->Just(2*y)) // // Nothing sails through, as we wanted: ghci> Nothing >>= \ x -> Just (x*x) >>= \ x -> Just ( x + 1 ) >>= \ y -> Just ( 2*y ) Nothing // Note that we never implicitly specified what to do with NaN, i.e., Nothing. We got this // code from the definition of Maybe: instance Monad Maybe where (Just x) >>= k = k x -- next function in the pipeline gets called on "unboxed" x Nothing >>= k = Nothing -- the Nothing sails through case return = Just fail s = Nothing // There is syntactic sugar for this, which I don't really like: ghci> let pipe n = do y <- Just (n*n) ; z <- Just (y + 1) ; Just (2*z) ghci| ghci> :t pipe pipe :: Num b => b -> Maybe b ghci> pipe 5 Just 52 // There is also a "return", also syntactic sugar ghci> let pipe n = do y <- Just (n*n) ; z <- Just (y + 1) ; return (2*z) ghci| ghci> :t pipe pipe :: Num b => b -> Maybe b ghci> pipe 5 Just 52 ghci> Just 5 >>= pipe Just 52 ghci> Nothing >>= pipe Nothing // The following doesn't typecheck, as it shouldn't: pipe takes the "unboxed" value ghci> pipe Nothing :130:1: error: [GHC-39999] • No instance for ‘Num (Maybe ())’ arising from a use of ‘it’ • In the first argument of ‘print’, namely ‘it’ In a stmt of an interactive GHCi command: print it ghci> :i Nothing type Maybe :: * -> * data Maybe a = Nothing | ... -- Defined in ‘GHC.Internal.Maybe’ ----------------------[ What about optimization & tail recursion? ]---------------------- // Some serious optimizations happen here (not a tail-recursive call!) ghci> let fc 0 = 1 ghci| fc n = n * fc (n-1) ghci| ghci> fc 5 120 ghci> fc 1000 4023872600...0000000000 ghci> fc 10000 28462596809170545189064132121198688901480514017027992307941799942744113400037644437729907867577847758158840621423175288300423399401535187390524211613827161748198241998275924182892597878981242531205946599625986706..000000000 ======================[ Algebraic data types ]======================= In Haskell, you are free (and expected to) construct data types---including functional data types---from the primitive ones. Whenever you write a function or a lambda or a partial application, you are, in fact, constructing a new type. GHCI will show you that time with :t, for example: ghci> :t (+) 1 (+) 1 :: Num a => a -> a (Recall that "let f = (+) 1 in f 2" gets you 3. GHCI will get you an error for "(+) 1" because it doesn't know how to convert it to a string to print it, but it's a valid value of a function type.) Think of this as having an additional language in which you write (create) formulas for types, similar to how you write formulas in algebra. Just like in algebra, you can use variables to signify unknowns, or parameters. Compare this with the formally defined grammar in the Ian Grant's paper mentioned above. Whenever you define a function that takes some object of type A to type B, you have constructed a type (A -> B). This serves as assurance that if you are given an object x of A, then B will not be an empty type, because you will use your function on x to get an object of B. This might remind you of logic: if you have a proposition A that you know to be true, and you know an implication A => B (from A follows B), then you can also obtain that B is true. The proof of B consists of showing A and A => B ; with the implication A => B, you know how to make (or, derive) a B out of A. These parallels between constructing function types (i.e., writing functions, i.e., programming) and proving logical theorems lead to the Curry-Howard Isomorphism, which is super-exciting. You can also make new types by extending the values of existing types---like one constructs new sets from given sets (think set theory and Venn diagrams). For example, with "Maybe a" you can take a type and extend it with a special value Nothing (usually meaning "an error occurred, but I'll deal with it later; don't terminate the program via an exception". With 'Either', you can have a type that contains values of two different types, which a unconfusable as to which type they came from---this is called a "direct sum" (you can do the same for two sets, but you need to watch out for values that occur in both, because, say, a 0 from the first set and a 0 from the second set will be two different elements of the direct sum of these number sets). For examples of Either, see https://tuttlem.github.io/2013/01/05/either-type-in-haskell.html You can also construct a "direct product" of two types---we know these as pairs (a,b) or tuples. Even though H.-M. type system does not allow us to mix different types in a list, we can do a List of Ether to much the same effect. Such are "algebraic types". Like formulas in algebra, these are endless; you can always write a longer (and valid) formula from existing ones.