lude

Haskell prelude alternative
git clone git://git.rr3.xyz/lude | git clone gits://git.rr3.xyz/lude
Log | Files | Refs | README | LICENSE

DependentKinds.hs (1333B)

      1 {-# LANGUAGE UndecidableInstances #-}
      2 {-# LANGUAGE UndecidableSuperClasses #-}
      3 
      4 module Todo.DependentKinds where
      5 
      6 import Lude
      7 
      8 --------------------------------------------------------------------------------
      9 
     10 type Forall :: forall k. (k -> Kind) -> Kind
     11 type Forall @k f = forall (a :: k). f a
     12 
     13 type (@->) :: forall k -> (k -> Kind) -> Kind
     14 type k @-> f = Forall @k f
     15 
     16 --------------------------------------------------------------------------------
     17 
     18 type Exists :: forall k. (k -> Kind) -> Kind
     19 data Exists _ where
     20     MkExists :: forall k (f :: k -> Kind). forall (a :: k) -> f a -> Exists @k f
     21 
     22 type (@*) :: forall k -> (k -> Kind) -> Kind
     23 type k @* f = Exists @k f
     24 
     25 type Idx :: forall k (f :: k -> Kind). Exists f -> k
     26 type family Idx _ where
     27     Idx (MkExists a _) = a
     28 
     29 type Val :: forall k (f :: k -> Kind). forall (e :: Exists f) -> f (Idx e)
     30 type family Val _ where
     31     Val (MkExists _ x) = x
     32 
     33 type OnIdx :: forall k (f :: k -> Kind). Predicate k -> Predicate (Exists f)
     34 class (p (Idx e)) => OnIdx p e
     35 instance forall k (f :: k -> Kind) (p :: Predicate k) (e :: Exists f). (p (Idx e)) => OnIdx p e
     36 
     37 type OnVal :: forall k (f :: k -> Kind). Forall (Predicate . f) -> Predicate (Exists f)
     38 class (p (Val e)) => OnVal p e
     39 instance forall k (f :: k -> Kind) (p :: Forall (Predicate . f)) (e :: Exists f). (p (Val e)) => OnVal p e