Extended type system...

ext-type-sys.hs

{-# LANGUAGE GADTs, TypeFamilies, DataKinds, PolyKinds, KindSignatures, TypeOperators, RankNTypes, UndecidableInstances, AllowAmbiguousTypes, ExistentialQuantification, StandaloneDeriving, UnicodeSyntax, Arrows, MultiParamTypeClasses, ScopedTypeVariables #-}

data Kind = Self
          | Kind `To` Kind

data SingleKind :: Kind -> * where
    SingleSelf :: SingleKind Self
    SingleTo   :: SingleKind a -> SingleKind b -> SingleKind (a `To` b)

instance Show (SingleKind (k :: Kind)) where
    show SingleSelf     = "*"
    show (SingleTo x y) = "(" ++ show x ++ " -> " ++ show y ++ ")"

self = SingleSelf
to   = SingleTo

data Type = Zero
          | One
          | All Type Type    {- forall  type : Type, (type -> Type) : Type -}
          | Exists Type Type {- there's type : Type, (type -> Type) : Type -}
          | Rec Type
          | Infinite         {- ~so ghc will not complain~ -}
          | Type `Sum` Type
          | Type `Prod` Type
          | Neg Type         {- a - b = a + (-b)  -}
          | Frac Type        {- a / b = a * (1/b) -}
          | Id Type          {- ((x : a) = (y : a)) : Id a -}

type family Try (a :: Type) (b :: Type) (initial :: Type) :: Type where
{-
    Try One  y i              = One
    Try Zero One i            = One
    Try Zero Zero i           = Zero
-}
    Try (Sum x y) (Sum w z) i = Try (Match x w i) (Match y z i) i
    Try Zero Zero i           = Zero
    Try a b i                 = One

type family Unloop (a :: Type) :: Type where
    Unloop (Rec x)      = x
    Unloop y            = y

{-
    Unloop Zero         = Zero
    Unloop One          = One
    Unloop (All x y)    = All x y
    Unloop (Exists x y) = Exists x y
    Unloop Infinite     = Infinite
    Unloop (Sum x y)    = Sum x y
    Unloop (Prod x y)   = Prod x y
    Unloop (Neg x)      = Neg x
    Unloop (Frac x)     = Frac x
-}

type family Whether (a :: Type) (b :: Type) (c :: Type) :: Type where
    Whether One  x y = x
    Whether Zero x y = y

type family Match (a :: Type) (b :: Type) (initial :: Type) :: Type where
    Match Zero x i                = Zero
    Match One One i               = One
    Match Infinite x i            = Match x i i
    Match (Prod x y) (Prod w z) i = Match (Match x w i) (Match y z i) i
    Match (Sum x y) (Sum w z) i   = Try (Match x w i) (Match y z i) i
    Match (Neg x) (Neg y) i       = Match x y i
    Match (Frac x) (Frac y) i     = Match x y i

data Value :: Type -> * where
    Unit    ::                       Value One
    Above   :: Value a ->            Value (Sum a b)
    Under   :: Value b ->            Value (Sum a b)
    Both    :: Value a -> Value b -> Value (Prod a b)
    Back    :: Value a ->            Value (Neg a)
    Proof   :: Value a ->            Value (Frac a)
    Same    :: Value a -> Value a -> Value (Id a)

instance Eq (Value (a :: Type)) where
    Unit       == Unit       = True
    (Above x)  == (Above y)  = x == y
    (Under x)  == (Under y)  = x == y
    (Both x y) == (Both w z) = x == w && y == z
    (Back x)   == (Back y)   = x == y
    (Proof x)  == (Proof y)  = x == y
    _          == _          = False

instance Show (Value (a :: Type)) where
    show Unit       = "*"
    show (Above x)  = "left " ++ show x
    show (Under y)  = "right " ++ show y
    show (Both x y) = "(" ++ show x ++ ", " ++ show y ++ ")"
    show (Back x)   = "(-" ++ show x ++ ")"
    show (Proof x)  = "(1/" ++ show x ++ ")"
    show (Same x y) = "(" ++ show x ++ " = " ++ show y ++ ")"

swapsum :: Value (Sum a b) -> Value (Sum b a)
swapsum (Above x) = Under x
swapsum (Under y) = Above y

swapprod :: Value (Prod a b) -> Value (Prod b a)
swapprod (Both x y) = Both y x

involback :: Value (Neg (Neg a)) -> Value a
involback (Back (Back x)) = x

involproof :: Value (Frac (Frac a)) -> Value a
involproof (Proof (Proof x)) = x

collect :: Value a -> Value (Frac a) -> Value One
collect _ _ = Unit

create :: Value One -> Value a -> Value (Prod a (Frac a))
create _ x = Both x (Proof x)

unfoldid :: Value (Id a) -> Value (Prod a a)
unfoldid (Same x y) = Both x y

mapid :: Value (Id a) -> (Value a -> Value b) -> (Value a -> Value b) -> Value (Id b)
mapid (Same x y) f g = Same (f x) (g y)

data SingleType :: Type -> Kind -> * where
    SingleZero   ::                                           SingleType Zero Self
    SingleOne    ::                                           SingleType One Self
    SingleAll    :: (SingleType a k -> SingleType b l) ->     SingleType (All a b) (k `To` l)
    SingleExists :: (SingleType a k -> SingleType b l) ->     SingleType (Exists a b) (k `To` l)
    SingleRec    :: SingleType a k ->                         SingleType (Rec a) k
    SingleLift   :: SingleType (Rec a) k ->                   SingleType Infinite k
    SingleSum    :: SingleType a Self -> SingleType b Self -> SingleType (Sum a b) Self
    SingleProd   :: SingleType a Self -> SingleType b Self -> SingleType (Prod a b) Self
    SingleNeg    :: SingleType a Self ->                      SingleType (Neg a) Self
    SingleFrac   :: SingleType a Self ->                      SingleType (Frac a) Self
    SingleId     :: SingleType a Self -> SingleType a Self -> SingleType (Id a) Self
    SingleCheck  :: SingleType a Self -> Value b ->           SingleType (Match (Unloop a) b (Unloop a)) Self

instance Eq (SingleType (a :: Type) (k :: Kind)) where
    SingleZero       == SingleZero = True
    SingleOne        == SingleOne  = True
    (SingleProd x y) == (SingleProd w z) = x == w && y == z
    (SingleSum x y)  == (SingleSum w z)  = x == w && y == z
    (SingleNeg x)    == (SingleNeg y)    = x == y
    (SingleFrac x)   == (SingleFrac y)   = x == y
    _ == _ = False

zero  = SingleZero
one   = SingleOne
param = SingleAll
(|+|) = SingleSum
(|*|) = SingleProd
inf   = SingleLift
defer = SingleRec

check :: (Match (Unloop a) b (Unloop a)) ~ One => SingleType a Self -> Value b -> SingleType One Self
check singletyp value = SingleCheck singletyp value

bool   = one |+| one
coprod = param (\a -> param (\b -> a |+| b))
prod   = param (\a -> param (\b -> a |*| b))
option = param (\a -> one |+| a)
nat    = let self = defer (one |+| (inf self)) in self
list   = param (\a -> let self = defer (one |+| (a |*| inf self)) in self)
btree  = param (\a -> let self = defer (one |+| ((inf self |*| a) |*| inf self)) in self)

{-
                 bool   = 1 + 1
  forall (a, b), sum    = a + b
  forall (a, b), prod   = a * b
  forall a,      option = 1 + a
                 nat    = 1 + nat
  forall a,      list   = 1 + (a * list)
  forall a,      btree  = 1 + (btree * a * btree)
-}

new :: SingleType (All a b) (To k l) -> SingleType a k -> SingleType b l
new (SingleAll depen) a = depen a

instance (Show (Value (a :: Type))) => Show (SingleType (a :: Type) (k :: Kind)) where
    show SingleZero        = "0"
    show SingleOne         = "1"
    show (SingleSum x y)   = "(" ++ show x ++ " + " ++ show y ++ ")"
    show (SingleAll _)     = "(forall...)"
    show (SingleExists _)  = "(there's...)"
    show (SingleRec _)     = "(recursive...)"
    show (SingleProd x y)  = "(" ++ show x ++ " + " ++ show y ++ ")"
    show (SingleNeg x)     = "(-" ++ show x ++ ")"
    show (SingleFrac x)    = "(1/" ++ show x ++ ")"
    show (SingleLift _)    = "(infinite...)"
    show (SingleCheck x y) = "(" ++ show y ++ " : " ++ show x ++ ")"
    show (SingleId x y)    = "(" ++ show x ++ " = " ++ show y ++ ")"

-- type for reversible functions |todo| --
data Comb :: Type -> Type -> * where
    Refl  ::                                           Comb a a
    Sym   :: Comb a b ->                               Comb b a
    Comp  :: Comb a b -> Comb b c ->                   Comb a c
    Add   :: Comb a b -> Comb c d ->                   Comb (Sum a c) (Sum b d)
    Mul   :: Comb a b -> Comb c d ->                   Comb (Prod a c) (Prod b d)
    Trace :: Comb (Sum a b) (Sum a c) ->               Comb b c
    Check :: Comb a b -> (Value a -> Value b) ->       Comb One One
    Map   :: SingleType a Self -> SingleType b Self -> Comb a b

class Iso prim comb where
    iso :: Maybe (prim a -> prim b) -> Maybe (prim b -> prim a) -> comb a b

type Choice = Sum One One
false :: Value Choice
false  = Above Unit
true  :: Value Choice
true   = Under Unit

type List a b = Sum One (Prod a b)
type Nil  a   = Value (List a (Sum One One))
type Cons a b = Value a -> Value b -> Value (List a b)
nil      :: Nil a
nil       = Above Unit
cons     :: Cons a b
cons x y  = Under $ Both x y

first :: (Value a -> Value a) -> Value (List a b) -> Value (List a b)
first f (Under (Both x y)) = Under $ Both (f x) y

rest :: (Value b -> Value b) -> Value (List a b) -> Value (List a b)
rest f (Under (Both x y)) = Under $ Both x (f y)

{-

*Main> cons true $ cons false nil
right (right *, right (left *, left *))

======================================================
*Main> first swapsum $ cons true $ cons false nil
right (left *, right (left *, left *))

========================================================
*Main> rest (first swapsum) $ cons true $ cons false nil
right (right *, right (right *, left *))

-}

x = check bool true
y = check (new list one)  $ cons Unit nil
z = check (new list bool) $ cons true $ cons false nil

is :: Match (Unloop b) a (Unloop b) ~ One => Value a -> SingleType b Self -> ( )
is _ _ = ( )

being :: Value a -> SingleType (Rec a) Self -> ( )
being _ _ = ( )

{-

*Main> :t param (\a -> param (\b -> param (\m -> new (new m a) b)))
param (\a -> param (\b -> param (\m -> new (new m a) b)))
  :: SingleType
       ('All a1 ('All a ('All ('All a1 ('All a b)) b)))
       ('To k1 ('To k ('To ('To k1 ('To k l)) l)))

=====================================================================
*Main> :t param (\m -> param (\a -> param (\b -> new (new m a) b)))
param (\m -> param (\a -> param (\b -> new (new m a) b)))
  :: SingleType
       ('All ('All a1 ('All a b)) ('All a1 ('All a b)))
       ('To ('To k1 ('To k l)) ('To k1 ('To k l)))

======================================================================
*Main> :t param (\m -> param (\a -> new m a)))

<interactive>:1:36: parse error on input ‘)’
*Main> :t param (\m -> param (\a -> new m a))
param (\m -> param (\a -> new m a))
  :: SingleType
       ('All ('All a b) ('All a b)) ('To ('To k l) ('To k l))

======================================================================
*Main> :t param (\m -> m)
param (\m -> m) :: SingleType ('All b b) ('To l l)

-}