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

• tweet

-- The free category
data Free :: Cat ob -> Cat ob where
  Base :: Free cat a a

  (:·) :: cat a b 
       -> Free cat b c
       -> Free cat a c
infixr :·

varp2 :: Free Work a b -> (El a -> El b)
varp2 = \case
  Base -> 
    id

  w :· ws -> 
    varp2 ws . varp w 

• tweet

import Prelude hiding (id, (.), Functor(..))

import Data.Singletons 
import Data.Singletons.Prelude.Tuple

type Cat ob = ob -> ob -> Type

type (==>) = Prod (->) (->)

data Prod :: Cat a -> Cat b -> Cat (a, b) where
  (:×:) :: acat a a'
        -> bcat b b'
        -> Prod acat bcat '(a, b) '(a', b')

class Functor (f :: d ~> c) where
  type Dom f :: Cat d
  type Cod f :: Cat c

  fmap :: Dom f a      b 
       -> Cod f (f@@a) (f@@b)

-- We need to parameterise the FST defunctionalized symbol with the
-- categories it operates over, so we can construct
--
--   type Dom (FST acat bcat) = Prod acat bcat
--   type Cod (FST acat bcat) = acat
data FST :: Cat a -> Cat b -> (a, b) ~> a
data SND :: Cat a -> Cat b -> (a, b) ~> b

type instance FST acat bcat `Apply` '(a, _) = a
type instance SND acat bcat `Apply` '(_, b) = b

instance Functor (FST acat bcat) where
  type Dom (FST acat bcat) = Prod acat bcat
  type Cod (FST acat bcat) = acat

  fmap :: Prod acat bcat ab a'b'
       -> acat (FST acat bcat @@ ab) (FST acat bcat @@ a'b')
  fmap ((f :×: _)) = f

instance Functor (SND acat bcat) where
  type Dom (SND acat bcat) = Prod acat bcat
  type Cod (SND acat bcat) = bcat

  fmap :: Prod acat bcat ab a'b'
       -> bcat (SND acat bcat @@ ab) (SND acat bcat @@ a'b')
  fmap ((_ :×: g)) = g

• tweet

{-# Language QuantifiedConstraints #-}

import Data.Kind
import Control.Applicative

class    (forall xx. cls xx => cls' xx) => (~=>) cls cls'
instance (forall xx. cls xx => cls' xx) => (~=>) cls cls'

data Key = Reg Int | Addr Int | IC

type Val = Int

type T  = Type
type TT = T -> T
type C  = Constraint

type Semantics cls a =
  forall öö. cls öö 
    => (Key -> öö Val)
    -> (Key -> öö Val -> öö ())
    -> Maybe (öö a)

(·:=) :: Int -> Int -> Semantics f ()
(reg ·:= addr) read write = Just $
  write (Reg reg) (read (Addr addr))

jmp :: Int -> Semantics Functor ()
(jmp offset) read write = Just $
  write IC (fmap (+ offset) (read IC))

-- Let's give it instances
newtype SEMANTICS :: (TT -> C) -> TT where
  S :: Semantics cls a -> SEMANTICS cls a

instance functor ~=> Functor => Functor (SEMANTICS functor) where
  fmap :: forall a a'. (a -> a') -> (SEMANTICS functor a -> SEMANTICS functor a')
  fmap f (S semantics) = S semantics' where

    semantics' :: Semantics functor a'
    semantics' read write = do
      öö_a <- semantics read write
      pure (fmap f öö_a)

  (<$) :: forall a b. a -> SEMANTICS functor b -> SEMANTICS functor a
  a <$ S semantics = S semantics' where

    semantics' :: Semantics functor a
    semantics' read write = do
      öö_b <- semantics read write
      pure (a <$ öö_b)

pure' :: Applicative f => a -> f a
pure' = pure

instance app ~=> Applicative => Applicative (SEMANTICS app) where
  pure :: forall a. a -> SEMANTICS app a
  pure a = S semantics where

    semantics :: Semantics app a
    semantics read write = Just (pure a) -- we can't use pure!!!

  (<*) :: forall a b. SEMANTICS app a -> SEMANTICS app b -> SEMANTICS app a
  S as <* S bs = S semantics where

    semantics :: Semantics app a
    semantics read write = do
      a <- as read write
      b <- bs read write
      Just a                    -- we can't use pure!!!

  (*>) :: forall a b. SEMANTICS app a -> SEMANTICS app b -> SEMANTICS app b
  S as *> S bs = S semantics where

    semantics :: Semantics app b
    semantics read write = do
      a <- as read write
      b <- bs read write
      Just b                    -- we can't use pure!!!

  liftA2 :: forall a b c
          . (a -> b -> c) 
         -> (SEMANTICS app a -> SEMANTICS app b -> SEMANTICS app c) 
  liftA2 f (S as) (S bs) = S semantics where

    semantics :: Semantics app c
    semantics read write = do   -- can't use liftA2 etc. because of limitations!
      a <- as read write
      b <- bs read write
      Just (liftA2 f a b)

  (<*>) :: forall a b c. 
           SEMANTICS app (a -> b)
        -> SEMANTICS app a
        -> SEMANTICS app b
  S fs <*> S as = S semantics where

    semantics :: Semantics app b
    semantics read write = do
      f <- fs read write
      a <- as read write
      Just (f <*> a)

• 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)