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

• twitter

-- · 1st argument: Values of the constructor 
-- · 2nd argument: The resulting type after matching, 
-- · 3rd argument: The type
--
-- This is taken from the 'total' library
-- 
--   https://hackage.haskell.org/package/total
-- 
-- just like applying the original 'on' to an optic
--
--   on _Left :: (a -> res) -> (Either Void b -> res) -> (Either a b -> res)
--   ón PLeft :: (a -> res) -> (Either Void b -> res) -> (Either a b -> res)
-- 
data PEither :: T -> T -> T -> T where
  PLeft  :: PEither a (Either Void b) (Either a b)
  PRight :: PEither b (Either a Void) (Either a b)

ón 
  :: PEither val after before
  -> (val    -> res)
  -> (after  -> res)
  -> (before -> res)

-- ón PLeft :: (a -> res) -> (Either Void b -> res) -> (Either a b -> res)
ón PLeft  handle els (Left  a) = handle a
ón PLeft  handle els (Right b) = els (Right b)

-- ón PRight :: (b -> res) -> (Either a Void -> res) -> (Either a b -> res)
ón PRight handle els (Left  a) = els (Left a)
ón PRight handle els (Right b) = handle b


on
    :: ((a -> Either a Void) -> (before -> Either val after))
    -> (val    -> o)
    -> (after  -> o)
    -> (before -> o)
on p f g x = case p Left x of
  Left  l -> f l
  Right r -> g r

-- https://twitter.com/Iceland_jack/status/1024873148469137408

import Control.Lens

type One   = Int
type Two   = Bool
type Three = Double

triple :: (One, Two, Three)
triple = (10, False, pi)

yo :: ASetter s t a b -> (s -> (a -> b) -> t)
yo = flip . over

yonedaOne   :: (One   -> one)   -> (one, Two, Three)
yonedaTwo   :: (Two   -> two)   -> (One, two, Three)
yonedaThree :: (Three -> three) -> (One, Two, three)

yonedaOne   = yo _1 triple
yonedaTwo   = yo _2 triple
yonedaThree = yo _3 triple

(Binary) Product categories are basically the product of two categories. Any two functions

one = const 'a' :: a   -> Char
two = show @Int :: Int -> String

can be written as a single arrow in the product category (->) × (->)

data (×) :: Cat a -> Cat b -> Cat (a, b) where
  (:×:) :: cat1 a1 b1
        -> cat2 a2 b2
        -> (cat1 × cat2) '(a1, a2) '(b1, b2)

pair :: ((->) × (->)) '(a, Int) '(Char, String)
pair = const 'a' :×: show @Int

Defining coproducts as an adjunction makes use of product categories, the functors go from product categories
It is used in the adjunction defining

type Hask = (->)

-- Diagonal :: k            -> (k, k)
-- Coprod   :: (Type, Type) -> Type

type family
  Diagonal (a :: k) = (res :: (k, k)) | res -> a where
  Diagonal a = '(a, a)

type family
  Coprod (pair :: (Type, Type)) = (res :: Type) | res -> pair where
  Coprod '(a, b) = Either a b

leftAdjunct :: Hask        (Coprod '(a1, a2)) b
            -> (Hask×Hask) '(a1, a2) (Diagonal b)
leftAdjunct elim = (elim . Left) :×: (elim . Right)

rightAdjunct :: (Hask×Hask) '(a1, a2) (Diagonal b)
             -> Hask        (Coprod '(a1, a2)) b
rightAdjunct (left :×: right) = either left right 

But what about a generalization for 0-, 1-, 2-, ... product categories? With this prelude:

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

data HList :: [Type] -> Type where
  HNil  :: HList '[]
  (::·) :: a
        -> HList    as
        -> HList (a:as)

data Cats :: [Type] -> Type where
  CNil  :: Cats '[]
  (:··) :: Cat ob 
        -> Cats obs
        -> Cats (ob:obs)

We go on to define the first attempt:

data Prod0 :: Cat [Type] where
  Base0 :: Prod0 '[] '[]
  Step0 :: Hask   a      b
        -> Prod0    as     bs
        -> Prod0 (a:as) (b:bs)

This only allows for (->) functions

prod0 :: Prod0 '[Int, Int] '[String, Bool]
prod0 = Base0
  & Step0 (== 0) 
  & Step0 show

The first and last type-level lists should always have the same length:

data Prod1 :: forall n. Cat (Vec n Type) where
  Base1 :: Prod1 VNil VNil
  Step1 :: Hask   a       b
        -> Prod1     as      bs
        -> Prod1 (a:·as) (b:·bs)

prod1 :: Prod1 (Int :· Int :· VNil) (String :· Bool :· VNil)
prod1 = Base1
  & Step1 (== 0) 
  & Step1 show

But we really want to allow for different categories, of different kinds? So one arrow might be between Nat objects

proof1 :: 0 ·<= 10
proof2 :: 5 ·<= 55

data Prod2 :: forall as. Cats as -> Cat (HList as) where
  Base2 :: Prod2 CNil HNil HNil
  Step2 :: cat a b
        -> Prod2 cats          as       bs
        -> Prod2 (cat:··cats) (a::·as) (b::·bs)

which allows different kinds

prod2 :: Category cat => 
  Prod2 
    (cat :··(·<=):··(·<=):··CNil) 
    (Char::·5    ::·0    ::·HNil)
    (Char::·55   ::·10   ::·HNil)
prod2 = Base2
  & Step2 Proof1
  & Step2 Proof2
  & Step2 id

(Binary) Product categories are basically the product of two categories. Any two functions

one = const 'a' :: a   -> Char
two = show @Int :: Int -> String

can be written as a single arrow in the product category (->) × (->)

data (×) :: Cat a -> Cat b -> Cat (a, b) where
  (:×:) :: cat1 a1 b1
        -> cat2 a2 b2
        -> (cat1 × cat2) '(a1, a2) '(b1, b2)

pair :: ((->) × (->)) '(a, Int) '(Char, String)
pair = const 'a' :×: show @Int

Defining coproducts as an adjunction makes use of product categories, the functors go from product categories
It is used in the adjunction defining

type Hask = (->)

-- Diagonal :: k            -> (k, k)
-- Coprod   :: (Type, Type) -> Type

type family
  Diagonal (a :: k) = (res :: (k, k)) | res -> a where
  Diagonal a = '(a, a)

type family
  Coprod (pair :: (Type, Type)) = (res :: Type) | res -> pair where
  Coprod '(a, b) = Either a b

leftAdjunct :: Hask        (Coprod '(a1, a2)) b
            -> (Hask×Hask) '(a1, a2) (Diagonal b)
leftAdjunct elim = (elim . Left) :×: (elim . Right)

rightAdjunct :: (Hask×Hask) '(a1, a2) (Diagonal b)
             -> Hask        (Coprod '(a1, a2)) b
rightAdjunct (left :×: right) = either left right 

But what about a generalization for 0-, 1-, 2-, ... product categories? With this prelude:

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

data HList :: [Type] -> Type where
  HNil  :: HList '[]
  (::·) :: a
        -> HList    as
        -> HList (a:as)

data Cats :: [Type] -> Type where
  CNil  :: Cats '[]
  (:··) :: Cat ob 
        -> Cats obs
        -> Cats (ob:obs)

We go on to define the first attempt:

data Prod0 :: Cat [Type] where
  Base0 :: Prod0 '[] '[]
  Step0 :: Hask   a      b
        -> Prod0    as     bs
        -> Prod0 (a:as) (b:bs)

This only allows for (->) functions

prod0 :: Prod0 '[Int, Int] '[String, Bool]
prod0 = Base0
  & Step0 (== 0) 
  & Step0 show

The first and last type-level lists should always have the same length:

data Prod1 :: forall n. Cat (Vec n Type) where
  Base1 :: Prod1 VNil VNil
  Step1 :: Hask   a       b
        -> Prod1     as      bs
        -> Prod1 (a:·as) (b:·bs)

prod1 :: Prod1 (Int :· Int :· VNil) (String :· Bool :· VNil)
prod1 = Base1
  & Step1 (== 0) 
  & Step1 show

But we really want to allow for different categories, of different kinds? So one arrow might be between Nat objects

proof1 :: 0 ·<= 10
proof2 :: 5 ·<= 55

data Prod2 :: forall as. Cats as -> Cat (HList as) where
  Base2 :: Prod2 CNil HNil HNil
  Step2 :: cat a b
        -> Prod2 cats          as       bs
        -> Prod2 (cat:··cats) (a::·as) (b::·bs)

which allows different kinds

prod2 :: Category cat => 
  Prod2 
    (cat :··(·<=):··(·<=):··CNil) 
    (Char::·5    ::·0    ::·HNil)
    (Char::·55   ::·10   ::·HNil)
prod2 = Base2
  & Step2 Proof1
  & Step2 Proof2
  & Step2 id

-- This defines our expression language
class Add a where (+·) :: a -> a -> a

class Zero a where zero :: a
class One  a where one  :: a
class Two  a where two  :: a

-- This is how we remove
--
--   two
--
-- replacing it with
--
--   one +· one
--
newtype ByeTwo a = ByeTwo a
  deriving newtype
    (One, Add, Zero)

instance (One a, Add a) => Two (ByeTwo a) where
  two :: ByeTwo a
  two = ByeTwo (one +· one)

-- One language without 'two'
-- One langauge with    'two'
type TwoNo  = (forall xx. (Add xx, Zero xx, One xx)         => xx)
type TwoYes = (forall xx. (Add xx, Zero xx, One xx, Two xx) => xx)

-- Here we remove 'two'
byeTwo :: TwoYes -> TwoNo 
byeTwo (ByeTwo bye) = bye

-- Here we write a concrete expression language
data E = Lit Int | E :+: E deriving Show
-- that has an instance for all of our classes
instance Add  E where (+·) = (:+:)
instance Zero E where zero = Lit 0
instance One  E where one  = Lit 1
instance Two  E where two  = Lit 2

-- >> four @E
-- Lit 2 :+: Lit 2
four :: TwoYes
four = two +· two

-- >> four' @E
-- (Lit 1 :+: Lit 1) :+: (Lit 1 :+: Lit 1)
four' :: TwoNo
four' = byeTwo four

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

infixr 5 
  :·

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

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

infixr 0
  --->

data (--->) :: forall n. Cat (Vec n Type) where
  Arr0 :: VNil ---> VNil
  ArrS :: (a -> b)
       -> (as ---> bs)
       -> (a:·as ---> b:·bs)

id_ :: forall (as :: Vec n Type). SingI as => (as ---> as)
id_ = go (sing @_ @as) where

  go :: forall bs. Sing bs -> (bs ---> bs)
  go = \case
    SVNil  -> Arr0
    s:%·ss -> ArrS id (go ss)

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)