--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--Module : Type.Dummies
--Author : Daniel Schüssler
--License : BSD3
--Copyright : Daniel Schüssler
--
--Maintainer : Daniel Schüssler
--Stability : Experimental
--Portability : Uses various GHC extensions
--
--------------------------------------------------------------------------------
--Description :
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module Type.Dummies where
#include "../Defs.hs"
-- | \"Kind-cast\" @ SET @ to @*@
data Lower (a :: SET)
-- | \"Kind-cast\" @ SET1 @ to @ SET @. Also lower elements using 'Lower'.
data Lower1 (a :: SET1) :: SET where
LowerElement :: u x -> Lower1 u (Lower x)
-- | \"Kind-cast\" @ SET2 @ to @ SET1 @. Also lower elements using 'Lower1'.
data Lower2 (a :: SET2) :: SET1 where
Lower1Element :: u x -> Lower2 u (Lower1 x)
-- | \"Kind-cast\" @ SET3 @ to @ SET2 @. Also lower elements using 'Lower2'.
data Lower3 (a :: SET3) :: SET2 where
Lower2Element :: u x -> Lower3 u (Lower2 x)
-- | Pair of types of kind @ SET @
data PAIR (a :: SET) (b :: SET) x
-- | Pair of types of kind @ SET1 @
data PAIR1 (a :: SET1) (b :: SET1) (x :: SET)
-- | Pair of types of kind @ SET2 @
data PAIR2 (a :: SET2) (b :: SET2) (x :: SET1)
-- | Pair of types of kind @ SET3 @
data PAIR3 (a :: SET3) (b :: SET3) (x :: SET2)
data Bool0
data Bool1
data BOOL :: SET where
Bool0 :: BOOL Bool0
Bool1 :: BOOL Bool1
elimBOOL :: BOOL a -> r Bool0 -> r Bool1 -> r a
elimBOOL Bool0 x _ = x
elimBOOL Bool1 _ x = x
kelimBOOL :: BOOL a -> r -> r -> r
kelimBOOL Bool0 x _ = x
kelimBOOL Bool1 _ x = x
-- data ΣPair (a :: SET) (b :: *)
-- type DependentPair = ΣPair
-- type Curry f a b = f (a,b)
-- type family Uncurry (f :: * -> * -> *) (ab :: *) :: *
-- type instance Uncurry g (a,b) = g a b
-- type Curry2 f a b = f (Pair2 a b)
-- type family Uncurry2 (g :: SET -> SET -> *) (ab :: SET) :: *
-- type instance Uncurry2 g (Pair2 a b) = g a b
-- type Curry3 f a b = f (Pair3 a b)
-- type family Uncurry3 (g :: SET1 -> SET1 -> *) (ab :: SET1) :: *
-- type instance Uncurry3 g (Pair3 a b) = g a b
-- type Curry4 f a b = f (Pair4 a b)
-- type family Uncurry4 (g :: SET2 -> SET2 -> *) (ab :: SET2) :: *
-- type instance Uncurry4 g (Pair4 a b) = g a b