summaryrefslogtreecommitdiff log msg author committer range
blob: e99c7b5dd58e8fe4dd06cb350f2b9827138a40e6 (plain)
 ```1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 ``` ``````{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies, TypeInType #-} {-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-} module RaeBlogPost where import Data.Kind -- a Proxy type with an explicit kind data Proxy k (a :: k) = P prox :: Proxy * Bool prox = P prox2 :: Proxy Bool 'True prox2 = P -- implicit kinds still work data A data B :: A -> * data C :: B a -> * data D :: C b -> * data E :: D c -> * -- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> * -- a kind-indexed GADT data TypeRep (a :: k) where TInt :: TypeRep Int TMaybe :: TypeRep Maybe TApp :: TypeRep a -> TypeRep b -> TypeRep (a b) zero :: TypeRep a -> a zero TInt = 0 zero (TApp TMaybe _) = Nothing data Nat = Zero | Succ Nat type family a + b where 'Zero + b = b ('Succ a) + b = 'Succ (a + b) data Vec :: * -> Nat -> * where Nil :: Vec a 'Zero (:>) :: a -> Vec a n -> Vec a ('Succ n) infixr 5 :> -- promoted GADT, and using + as a "kind family": type family (x :: Vec a n) ++ (y :: Vec a m) :: Vec a (n + m) where 'Nil ++ y = y (h ':> t) ++ y = h ':> (t ++ y) -- datatype that mentions * data U = Star (*) | Bool Bool -- kind synonym type Monadish = * -> * class MonadTrans (t :: Monadish -> Monadish) where lift :: Monad m => m a -> t m a data Free :: Monadish where Return :: a -> Free a Bind :: Free a -> (a -> Free b) -> Free b -- yes, * really does have type *. type Star = (* :: (* :: (* :: *))) ``````