(Reachable = explicitly used, or in another constraint with a reachable variable.) ~~~~ {.haskell} sym :: forall a. Eq a => Int -- illegal ~~~~ * Every constraint must have a type variable ~~~~ {.haskell} sym :: Eq Int => Bool -- illegal ~~~~ # Monad classes * It's neat that `liftIO` works from so many monads * Why not do something similar for `StateT`? Make `get`/`set` methods ~~~~ {.haskell} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} -- Saw this very briefly in Monad lecture: class (Monad m) => MonadState s m where get :: m s put :: s -> m () instance (Monad m) => MonadState s (StateT s m) where get = StateT $ \s -> return (s, s) put s = StateT $ \_ -> return ((), s) ~~~~ * Now for each other `MonadTrans`, pass requests down * This is just like `liftIO`. E.g., for `ReaderT`: ~~~~ {.haskell} instance (MonadIO m) => MonadIO (ReaderT r m) where liftIO = lift . liftIO instance (MonadState s m) => MonadState s (ReaderT r m) where get = lift get put = lift . put ~~~~ # Problem: we've defeated type inference * Remember `countLines`? ~~~~ {.haskell} doline (Left (SomeException _)) = get doline (Right _) = do n <- get; put (n + 1); go ~~~~ * The compiler knows we are in `StateT Int IO` monad * So can infer that the type of `get` is `StateT Int IO s` * But need to know `s` in order to select an instance of `MonadState`! * For all compiler knows, might be other matching instances, e.g., ~~~~ {.haskell} instance MonadState Double (StateT Int IO) where -- would be legal, but exists only in compiler's imagination ~~~~ * Since compiler can't infer return type of `get`, must type it manually: ~~~~ {.haskell} doline (Left (SomeException _)) = get :: StateT Int IO Int doline (Right _) = do n <- get; put ((n :: Int) + 1); go ~~~~ * Yuck! Lack of type inference gets old fast! # [`FunctionalDependencies`][] extension * Widely used & frowned upon (not as bad as `OverlappingInstances`) * Also referred to as "fundeps" * Lets a class declare some parameters to be functions of others ~~~~ {.haskell} class (Monad m) => MonadState s m | m -> s where get :: m s put :: s -> m () ~~~~ * The best way to think of this is in terms of *instance selection* * "`| m -> s`" says can select an instance based on `m` without considering `s`, because **`s` is a function of `m`** * Once you've selected the instance, you can use `s` for type inference * Disallows conflicting instances (even w. `OverlappingInstances`) * Also allows arbitrary computation at the type level [[Hallgren]][funWithFundeps] * But language committee wants compilation to be decidable and deterministic * So need to add some restrictions # [Sufficient conditions of decidable instances][instanceRules] * Anatomy of an instance: `instance` [*context* `=>`] *head* [`where` *body*] * *context* consists of zero or more comma-separated *assertions* 1. The Paterson Conditions: for each assertion in the context a. No type variable has more occurrences in the assertion than in the head ~~~~ {.haskell} class Class a b | a -> b instance (Class a a) => Class [a] Bool -- bad: 2 * a => 1 * a instance (Class a b) => Class [a] Bool -- bad: 1 * b => 0 * b ~~~~ b. The assertion has fewer constructors and variables than the head ~~~~ {.haskell} instance (Class a Int) => Class a Integer -- bad: 2 => 2 ~~~~ 2. The Coverage Condition: For each fundep *left* `->` *right*, the types in *right* cannot have type variables not mentioned in *left* ~~~~ {.haskell} class Class a b | a -> b instance Class a (Maybe a) -- ok: a "covered" by left instance Class Int (Maybe b) -- bad: b not covered instance Class a (Either a b) -- bad: b not covered ~~~~ # Undecidable vs. exponential -- who cares? * Editorial: maybe decidability of language is overrated * Computers aren't Turing machines with infinite tapes, after all * This legal, decidable program will crash your Haskell compiler ~~~~ {.haskell} crash = f5 () where f0 x = (x, x) -- type size 2^{2^0} f1 x = f0 (f0 x) -- type size 2^{2^1} f2 x = f1 (f1 x) -- type size 2^{2^2} f3 x = f2 (f2 x) -- type size 2^{2^3} f4 x = f3 (f3 x) -- type size 2^{2^4} f5 x = f4 (f4 x) -- type size 2^{2^5} ~~~~ * While plenty of not provably decidable programs happily compile * The conditions of the last slide are *sufficient*, not *necessary* * Might have other ways of knowing your program can compile * Or maybe figure it out from trial and error? # [`UndecidableInstances`][] extension * Lifts the Paterson and Coverage conditions * Also enables `FlexibleContexts` when enabled * Instead, imposes a maximum recursion depth * Default maximum depth is 20 * Can increase with `-fcontext-stack=`*n* option, e.g.: ~~~~ {.haskell} {-# OPTIONS_GHC -fcontext-stack=1024 #-} {-# LANGUAGE UndecidableInstances #-} ~~~~ * A bit reminiscent of C++ templates * gcc has a `-ftemplate-depth=` option * Note C++0x raises minimum depth from 17 to 1024 * Similarly, people have talked of increasing GHC's default context-stack # `MonadIO` revisited * Recall definition of `MonadIO` ~~~~ {.haskell} class (Monad m) => MonadIO m where liftIO :: IO a -> m a instance MonadIO IO where liftIO = id ~~~~ * Currently must define an instance for every transformer ~~~~ {.haskell} instance MonadIO (StateT s) where liftIO = lift . liftIO instance MonadIO (ReaderT t) where liftIO = lift . liftIO instance MonadIO (WriterT w) where liftIO = lift . liftIO ... ~~~~ * With `UndecidableInstances`, one instance can cover all transformers! ~~~~ {.haskell} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} -- undecidable: assertion Monad (t m) no smaller than head instance (MonadTrans t, MonadIO m, Monad (t m)) => MonadIO (t m) where liftIO = lift . liftIO ~~~~ # Summary of extensions * We've seen 6 typeclass-related extensions ~~~~ {.haskell} {-# LANGUAGE MultiParamTypeClasses #-} -- very conservative {-# LANGUAGE FlexibleInstances #-} -- conservative {-# LANGUAGE FlexibleContexts #-} -- conservative {-# LANGUAGE FunctionalDependencies #-} -- frowned upon {-# LANGUAGE UndecidableInstances #-} -- very frowned upon {-# LANGUAGE OverlappingInstances #-} -- the most controversial ~~~~ * Not all of these are looked upon kindly by the community * But if you enable all six, can be very powerful * Remainder of lecture looks at what you can do with all 6 enabled * Much inspired by [[Hlist]][] and [[OOHaskell]][] # Type-level natural numbers ~~~~ {.haskell} data Zero = Zero -- Type-level 0 data Succ n = Succ n -- Type-level successor (n + 1) class NatPlus a b c | a b -> c, a c -> b where natPlus :: a -> b -> c natMinus :: c -> a -> b instance NatPlus Zero a a where natPlus _ a = a natMinus a _ = a -- Note failure of coverage condition below instance (NatPlus a b c) => NatPlus (Succ a) b (Succ c) where natPlus (Succ a) b = (Succ (natPlus a b)) natMinus (Succ c) (Succ a) = natMinus c a ~~~~ * Fundeps + Context let us compute recursively on types! * If context has assertion `NatPlus a b c`, then from types `Succ a` and `b` we can compute `Succ c` (computation at type level) # Type-level booleans ~~~~ {.haskell} data HFalse = HFalse deriving Show data HTrue = HTrue deriving Show class HNot a b | a -> b where hnot :: a -> b instance HNot HFalse HTrue where hnot _ = HTrue instance HNot HTrue HFalse where hnot _ = HFalse class HEven a b | a -> b where hEven :: a -> b instance HEven Zero HTrue where hEven _ = HTrue instance (HEven n b, HNot b nb) => HEven (Succ n) nb where hEven (Succ n) = hnot (hEven n) ~~~~ ~~~~ *Main> hEven Zero HTrue *Main> hEven (Succ Zero) HFalse *Main> hEven (Succ (Succ Zero)) HTrue *Main> hEven (Succ (Succ (Succ Zero))) HFalse ~~~~ * Note how we use assertion `HNot b nb` to compute negation of `b` # Computing over types * Haven't used `OverlappingInstances` yet, let's start... * Can we compute whether two types are equal? First attempt: ~~~~ {.haskell} class TypeEq a b c | a b -> c where typeEq :: a -> b -> c instance TypeEq a a HTrue where typeEq _ _ = HTrue instance TypeEq a b HFalse where typeEq _ _ = HFalse ~~~~ * Problem: `TypeEq a a HTrue` not more specific than `TypeEq a b HFalse` * ... but it is more specific than `TypeEq a b c` * Recall that context is never consulted for instance selection * Only afterwards to reject failed assertions or infer types from fundeps * Solution: compute `c` after instance selection with another fundep ~~~~ {.haskell} class TypeCast a b | a -> b where typeCast :: a -> b instance TypeCast a a where typeCast = id instance TypeEq a a HTrue where typeEq _ _ = HTrue -- as before instance (TypeCast HFalse c) => TypeEq a b c where typeEq _ _ = typeCast HFalse ~~~~ # The utility of `TypeEq` * Editorial: `TypeEq` is kind of the holy grail of fundeps * Means you can program recursively at the type level * If you can implement `TypeEq`, you can distinguish base and recursive cases * But relies deeply on `OverlappingInstances`... * Example: Let's do for `MonadState` what we did for `MonadIO` ~~~~ {.haskell} instance (Monad m) => MonadState s (StateT s m) where get :: m s put :: s -> m () instance (MonadTrans t, MonadState s m, Monad (t m)) => MonadState s (t m) where get = lift get put = lift . put ~~~~ * `MonadIO` was easier because type `IO` can't match parameter `(t m)` * Unfortunately, `StateT s m` matches *both* of above instance heads * So need `OverlappingInstances` to select first instance for `StateT s m` # Heterogeneous lists * Last extension: [`TypeOperators`][] allows infix types starting with "`:`" ~~~~ {.haskell} data a :*: b = Foo a b type a :+: b = Either a b ~~~~ * Let's use an infix constructor to define a heterogeneous list ~~~~ {.haskell} data HNil = HNil deriving Show data (:*:) h t = h :*: !t deriving Show infixr 9 :*: -- Example: data A = A deriving Show data B = B deriving Show data C = C deriving Show foo = (A, "Hello") :*: (B, 7) :*: (C, 3.0) :*: HNil ~~~~ ~~~~ *Main> foo (A,"Hello") :*: ((B,7) :*: ((C,3.0) :*: HNil)) *Main> :t foo foo :: (A, [Char]) :*: ((B, Integer) :*: ((C, Double) :*: HNil)) ~~~~ # Operations on heterogeneous lists * Notice our list consisted of pairs ~~~~ {.haskell} foo :: (A, [Char]) :*: (B, Integer) :*: (C, Double) :*: HNil foo = (A, "Hello") :*: (B, 7) :*: (C, 3.0) :*: HNil ~~~~ * View first element as a key or tag, second as a value--How to look up value? ~~~~ {.haskell} class Select k h v | k h -> v where (.!) :: h -> k -> v instance Select k ((k, v) :*: t) v where (.!) ((_, v) :*: _) _ = v instance (Select k h v) => Select k (kv' :*: h) v where (.!) (kv' :*: h) k = h .! k ~~~~ ~~~~ *Main> foo .! A "Hello" ~~~~ * Once again, note the importance of `OverlappingInstances` * Needed to break recursion when type of lookup tag matches head of list * Can use to implement all sorts of other features (concatenation, etc.) # Object-oriented programming * Heterogeneous can implement object-oriented programming! ~~~~ {.haskell} returnIO :: a -> IO a returnIO = return data GetVal = GetVal deriving Show data SetVal = SetVal deriving Show data ClearVal = ClearVal deriving Show mkVal n self = do val <- newIORef (n :: Int) returnIO $ (GetVal, readIORef val) :*: (SetVal, writeIORef val) :*: (ClearVal, self .! SetVal $ 0) :*: HNil test = do -- prints 7, then 0 x <- mfix $ mkVal 7 x .! GetVal >>= print x .! ClearVal x .! GetVal >>= print ~~~~ * But why `mfix`? # "Tying the recursive knot" * `mfix` allows you to override methods with inheritance * Example, create a "const val" that ignores `SetVal` messages ~~~~ {.haskell} mkConstVal n self = do super <- mkVal n self returnIO $ (SetVal, const $ return ()) :*: super test2 = do x <- mfix $ mkConstVal 7 x .! GetVal >>= print x .! ClearVal x .! GetVal >>= print ~~~~ ~~~~ *Main> test 7 0 *Main> test2 7 7 ~~~~ * `mkVal`'s call to `SetVal` was properly overridden by `mkConstVal` [LanguageOptions]: http://www.haskell.org/ghc/docs/latest/html/users_guide/flag-reference.html#id491691 [instanceRules]: http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#instance-rules [erkok]: http://citeseer.ist.psu.edu/viewdoc/download;jsessionid=13851C3A2D4F33918B9D662C20F30762?doi=10.1.1.43.5313&rep=rep1&type=pdf [mdo]: https://sites.google.com/site/leventerkok/recdo.pdf?attredirects=0 [typeclasses]: http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-760004.3.1 [instances]: http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-770004.3.2 [funWithFundeps]: http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=D19C7E3BD1B5C1FC24035542B1494ED9?doi=10.1.1.22.7806&rep=rep1&type=pdf [`MonadFix`]: http://hackage.haskell.org/packages/archive/base/latest/doc/html/Control-Monad-Fix.html#t:MonadFix [`ExistentialQuantification`]: http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#existential-quantification [`MultiParamTypeClasses`]: http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#id559142 [`Rank2Types`]: http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#universal-quantification [`DoRec`]: http://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-extns.html#recursive-do-notation [`FlexibleInstances`]: http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#instance-decls [`OverlappingInstances`]: http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#instance-overlap [`FunctionalDependencies`]: http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#functional-dependencies [`FlexibleContexts`]: http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#flexible-contexts [`UndecidableInstances`]: http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#undecidable-instances [`TypeOperators`]: http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#infix-tycons [[HList]]: http://homepages.cwi.nl/~ralf/HList/paper.pdf [[OOHaskell]]: http://homepages.cwi.nl/~ralf/OOHaskell/paper.pdf