TypeLevelDoodle.hs

{-# LANGUAGE DataKinds #-}
data Cell m a b = ...

instance Monad m => Arrow (Cell m) where
  arr :: (a -> b) -> Cell m a b
  (***) :: Cell m  a1       b1
        -> Cell m      a2       b2
        -> Cell m (a1, a2) (b1, b2)

instance Monad m => Functor (Cell m a) where
  fmap f cell = cell >>> arr f

data Kleisli m a b = Kleisli (a -> m b)



instance Monad (r ->) where

instance Arrow (Kleisli (r ->)) where ...

Kleisli (r ->) a b == a -> (r -> b)

type ShowList = [forall a . Show a => a]

   Int -> (forall b . b)
== forall b . (Int -> b)
== Int -> b

(forall A . A) -> Int
== exists A . (A -> Int)

data ShowBox = forall a . Show a => ShowBox a

data ShowBox where
  ShowBox :: forall a . Show a => a -> ShowBox

data Exp
  = Number Int
  | Plus (Exp Int) (Exp Int)
  | Eq   (Exp Int) (Exp Int)

data Exp a where
  Number :: Int -> Exp Int
  Plus :: Exp Int -> Exp Int -> Exp Int
  Eq :: Exp Int -> Exp Int -> Exp Bool

val :: Exp a -> a
val (Number i) = i
val (Plus e1 e2) = val e1 + val e2
val (Eq e1 e2) = val e1 == val e2

mkShowBox :: Bool -> ShowBox
mkShowBox True = ShowBox 23
mkShowBox False = ShowBox (Just 4.5)

merge :: [ShowBox] -> ShowBox

(A : Set, a : A) -> Int
== (A : Set) -> (a : A) -> Int

(a, b) -> Int
== a -> (b -> Int)

myShow :: (forall a . Show a => a) -> String
myShow = show

let show' = show in show' 1 ++ show' [1]

type Negation = (-> Empty)

data Nat = Z | S Nat

data Vector (n :: Nat) a where
  VNil :: Vector Z a
  VCons :: a -> Vector n a -> Vector (S n) a

castLength :: Proxy n -> Vector m a -> Maybe (Vector n a)

data Proxy n = Proxy

class GetNat (n :: Nat) where
  getNat :: Proxy n -> Int

instance GetNat Z where
  getNat _ = 0

instance GetNat n => GetNat (S n) where
  getNat proxy = 1 + proxyPredecessor proxy

vecProxy :: Vec n a -> Proxy n
vecProxy _ = Proxy

vecLength :: Vec n a -> Int
vecLength = getNat . vecProxy

proxyPredecessor :: Proxy (S n) -> Proxy n
proxyPredecessor _ = Proxy