For Chris Allen, braindump

Braindump.hs

-- type Sig k = [k] -> Type
-- 
-- data AST :: Sig k -> Sig k where
--   Sym  :: dom a -> AST dom a
--   (:$) :: AST dom (a:as) -> AST dom '[a] -> AST dom as

singletons [d| data N = O | S N |]

infixr 5 :·
data Vec :: N -> Type -> Type where
  No    :: Vec O a
  (:·) :: a -> Vec n a -> Vec (S n) a

data Expr :: forall n. Vec n Type -> Type -> Type where
  A :: Expr No                 Int
  B :: Expr (Bool:·Double:·No) Int

  C1 :: Expr No (Int -> Int -> Int)
  C2 :: Expr (Int:·Int:·No) Int
  C3 :: Expr No Int -> Expr No Int -> Expr No Int

  NEG :: Expr (Int:·No) Int
  INT :: Int 
      -> Expr No Int

  BOOL :: Bool   -> Expr No Bool
  DBL  :: Double -> Expr No Double

  (:-) :: Expr (a:·as) res
       -> Expr No      a
       -> Expr as      res

type family
  ToFun_ n (as :: Vec n Type) a = (res :: Type) | res -> n as a where
  ToFun_ O     No      res = Full res
  ToFun_ (S n) (a:·as) res = a -> ToFun_ n as res

newtype Full a = Full a
  deriving newtype 
    (Num, Enum, Real, Integral, Eq, Ord)

type family
  DeFull a where
  DeFull (Full a) = a
  DeFull (a -> b) = a -> DeFull b

type Len (xs :: Vec n a) = n

type ToFun as a = ToFun_ (Len as) as a

eval :: Expr as a -> ToFun as a
eval = \case
  A -> 10

  B -> \case
    False -> round

    True -> const 5

  BOOL bool -> 
    Full bool

  DBL double -> 
    Full double

  (eval -> f) :- (eval -> Full a) -> 
    f $ a

  NEG -> 
    Full . negate

  INT i ->
    Full i

  C1 -> 
    Full (\a b -> a + b)

  C2 -> 
    \a b -> Full (a + b)

  C3 a b -> 
    eval a + eval b

N-ary product of categories

data Vec :: N -> TT where
  VecO :: Vec O a
  VecS :: a -> Vec n a -> Vec (S n) a

data (<=·) :: Cat Nat where
  LTE :: a <=  b
      => a <=· b

newtype (>=·) :: Cat Nat where
  GTE :: (<=·) a b -> (>=·) a b

data Cats :: forall n. Vec n T -> T where
  CatsO :: Cats VecO
  CatsS :: Cat ob
        -> Cats obs
        -> Cats (VecS ob obs)

data HList :: forall n. Vec n T -> T where
  HListO :: HList VecO
  HListS :: a -> HList as -> HList (VecS a as)

data NProd :: forall n (vec :: Vec n T). Cats vec -> Cat (HList vec) where
  NProdO
    :: NProd CatsO HListO HListO

  NProdS
    :: cat a b
    -> NProd cats as bs
    -> NProd (CatsS cat cats) (HListS a as) (HListS b bs)

nil :: NProd CatsO HListO HListO
nil = NProdO

one :: cat a a'
    -> NProd (CatsS cat CatsO) (HListS a HListO) (HListS a' HListO) 
one f = NProdS f NProdO

two :: cat  a a'
    -> cat' b b'
    -> NProd (CatsS cat (CatsS cat' CatsO))
         (HListS a (HListS b HListO))
         (HListS a' (HListS b' HListO))
two f g = NProdS f (NProdS g NProdO)