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

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

infixr 5
  :·, ·

type (·) = (:·)

data Vec :: N -> TT where
  X    :: Vec O a
  (:·) :: a -> Vec n a -> Vec (S n) a

data instance Sing (vec :: Vec n a) where
  SX    :: Sing X
  (:%·) :: Sing a -> Sing as -> Sing (a:·as)

instance SingI X where
  sing = SX

instance (SingI a, SingI as) => SingI (a:·as) where
  sing = sing :%· sing

-- First we introduce an n-ary product of the (->) category
--
-- (a1·a2·a3·X) ===> (b1·b2·b3·X)
--   =
-- (a1 -> b1) ×
-- (a2 -> b2) ×
-- (a3 -> b3)
--
infixr 5 
  `ArrsS`

infixr 9
  ===>

data (===>) :: forall n. Cat (Vec n T) where
  ArrsO :: X ===> X
  ArrsS :: (a -> b)
        -> (as ===> bs)
        -- ____________________
        -> (a:·as) ===> (b:·bs)

-- Examples of it
--
revRev :: ([a]·[b]·X) ===> ([a]·[b]·X)
revRev = reverse `ArrsS` reverse `ArrsS` ArrsO

-- Witnessing the adjunction between two functors
-- 
--   Coprod :: Vec n Type -> Type
--   Dup    :: Vec n Type <- Type
-- 
-- going between
-- 
--   FunctorOf (===>)  (->)  Coprod
--   FunctorOf  (->)  (===>) Dup
-- 

data Coprod :: forall n. Vec n T -> T where
  Here  :: a         
        -- ______________
        -> Coprod (a:·as)
  There :: Coprod as
        -- ______________
        -> Coprod (a:·as)

type family
  Dup (a :: T) :: Vec n T where
  Dup a = X
  Dup a = a · Dup a

absurdCoprod :: Coprod X -> b
absurdCoprod = \case

-- instance Functor Coprod where
--   type Dom Coprod = (===>)
--   type Cod Coprod = (->)
-- 
fmapCoprod :: (as ===> as') -> (Coprod as -> Coprod as')
fmapCoprod ArrsO        = absurdCoprod
fmapCoprod (ArrsS f fs) = \case
  Here a -> 
    Here (f a)
  There as -> 
    There (fmapCoprod fs as)

-- instance Functor Dup where
--   type Dom Dup = (->)
--   type Cod Dup = (===>)
-- 
fmapDup :: SN n -> (a -> a') -> (Dup a :: Vec n T) ===> Dup a'
fmapDup SO      f = ArrsO
fmapDup (SS sn) f = f `ArrsS` fmapDup sn f

-- OK so here is the adjunction, ready for it?
--
-- If L is left adjoint to R, then we can replace an L on the left
-- 
--   L a -> b
-- 
-- with an R on the right
-- 
--   a -> R b
--
-- such that they are isomorphic.

leftAdj :: forall as b
         . Sing as
        -> (Coprod as -> b)
        -> (as ===> Dup b)
leftAdj SX       elim                     = ArrsO
leftAdj (a:%·as) (hereElim :|: thereElim) = hereElim `ArrsS` leftAdj as thereElim

pattern (:|:) :: (a -> b) -> (Coprod as -> b) -> (Coprod (a·as) -> b)
pattern a :|: as <- ((Here >) &&& (There >) -> (a, as))

rightAdj :: (as ===> Dup b)
         -> (Coprod as -> b)
rightAdj = \case
  ArrsO -> 
    absurdCoprod
  ArrsS f fs -> 
    \case
      Here a -> f a
      There as -> rightAdj fs as

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)