{-# language UndecidableInstances #-} {-# language TypeFamilyDependencies #-} {-# language AllowAmbiguousTypes #-} {-# language UndecidableSuperClasses #-} {-# language MultiParamTypeClasses #-} module Data.Microgroove.TypeLevel where import GHC.Exts (Constraint) import GHC.TypeLits -- | Index into a type level list type family ((xs :: [u]) !! (n :: Nat)) where (x ': _) !! 0 = x (_ ': xs) !! n = xs !! (n-1) type family Length (xs :: [u]) :: Nat where Length '[] = 0 Length (_ ': xs) = 1 + Length xs -- | @AllF c f xs@ ensures that constraint @c (f x)@ holds for all @x@ in @xs@ type family AllF (c :: * -> Constraint) (f :: u -> *) (xs :: [u]) :: Constraint where AllF c f '[] = () AllF c f (x ': xs) = (c (f x),AllF c f xs) -- | Append type level lists type family (as :: [k]) ++ (bs :: [k]) where '[] ++ bs = bs (a ': as) ++ bs = a ': (as ++ bs) -- | Extend a type @x@ into a type level list @xs@ of length @n@ type family Replicate (n :: Nat) (x :: u) :: [u] where Replicate 0 x = '[] Replicate n x = x ': Replicate (n-1) x -- | Inductive Natural Numbers {-data Nat' = Z | S Nat'-} -- | An injective form of @Replicate@ using inductive @Nat'@ rather than builtins {-type family Replicate' (n :: Nat') (x :: u) = xs | xs -> n where-} {-Replicate' 'Z _ = '[]-} {-Replicate' ('S n) x = x ': Replicate' n x-} -- | The Existential Type @Some f@ is some @f x@ where @x@ is known at runtime data Some f where Some :: f x -> Some f -- | Avoids one indirection compared with @Maybe (Some f)@ data MaybeSome f = forall x. JustSome (f x) | None type family SetAt n xs x where SetAt 0 (_ ': xs) x = x ': xs SetAt n (x ': xs) y = x ': SetAt (n-1) xs y