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

remixing ideas from A Generic Abstract Syntax Model for Embedded Languages and Richard Eisenberg's Stitch: The Sound Type-Indexed Type Checker

https://twitter.com/Iceland_jack/status/996046261840175105

Finally tagless: dom is polykinded, so Add has a higher-rank kind

class Add (dom :: forall n. Vec n Type -> Type -> Type) where
  add1 :: dom No (Int -> Int -> Int)
  add2 :: dom (Int:·Int:·No) Int

newtype Eval args res = Eval (ToFun args res)

instance Add Eval where
  add1 :: Eval No (Int -> Int -> Int)
  add1 = Eval (Full (+))

  add2 :: Eval (Int:·Int:·No) Int
  add2 = Eval (\a b -> Full (a + b))

and without Full

newtype DeFullEval args res = DeFullEval (DeFull (ToFun args res))

instance X DeFullEval where
  a :: DeFullEval No (Int -> Int -> Int)
  a = coerce (a @Eval)

  b :: DeFullEval (Int:·Int:·No) Int
  b = coerce (b @Eval)

"Imagine if you couldn't simplify a+a to 2*a, that's how I feel in your language"

• tweet
• pdf A Type and Scope Safe Universe of Syntaxes with Binding Their Semantics and Proofs
• pdf Stitch: The Sound Type-Indexed Type Checker

infixr 0 ·>·
infixl 9 |-

--     (·×·)     : (a -> Type) -> (a -> Type) -> (a -> Type)
type (f ·×· g) a = (f a, g a)

--     (·>·)     : (a -> Type) -> (a -> Type) -> (a -> Type)
type (f ·>· g) a = f a -> g a

--     (|-)     : (a -> b) -> (b -> c) -> (a -> c)
type (f |- g) a = g (f a)

--   Konst     : a -> b -> a
type Konst a b = a

--   Forall   : (a -> b) -> b
type Forall f = forall xx. f xx

type Scoped a = forall nn. a -> Vec nn a -> Type

data N = O | S N

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

data Var :: Scoped a where
  VO :: Var i (i:>is) 
  VS :: Var i is -> Var i (j:>is)

o :: Forall ((:>) i |- Var i)
o = VO

s :: Forall (Var i ·>· (:>) j |- Var i)
s = VS

data Lam :: Scoped Type where
  V :: Var a as -> Lam a as
  A :: Lam (a -> b) as -> Lam a as -> Lam b as
  L :: Lam a (b:>as) -> Lam (a -> b) as

-- variable
v :: Forall (Var as ·>· Lam as)
v = V

-- application
a :: Forall (Lam (a -> b) ·>· Lam a ·>· Lam b)
a = A

-- lambda
l :: Forall ((:>) b |- Lam a ·>· Lam (a -> b))
l = L

• tweet
• GHC users guide

data A   = A0
data AB  = A1 | B1
data ABC = A2 | B2 | C2

type family
  AorB a :: Bool where
  AorB A  = True
  AorB AB = True
  AorB _  = False

data OnlyAB :: forall ab. AorB ab ~ True => ab -> Type where
  OnlyA0 :: OnlyAB A0
  OnlyA1 :: OnlyAB A1

  OnlyB1 :: OnlyAB B1

None of the *2 constructors could be used.

import Data.Kind
import Data.Coerce
import Data.Functor.Identity
import Data.Functor.Compose

class    Empty a
instance Empty a

class    (f a, g a) => (f & g) a
instance (f a, g a) => (f & g) a

class    (forall x. f x => g x) => (f ~=> g)
instance (forall x. f x => g x) => (f ~=> g)

-- class    (forall x y. f x y => g x y) => (f ~~=> g)
-- instance (forall x y. f x y => g x y) => (f ~~=> g)
-- class (a => b) => Implies a b
-- instance (a => b) => Implies a b


data Nat = Zero | Succ Nat

data Vec :: Type -> Nat -> Type where
  VNil :: Vec a Zero
  (:>) :: a -> Vec a n -> Vec a (Succ n)
infixr 5 :>

deriving instance Show a => Show (Vec a n)

type Scoped  a = forall nn. Vec a       nn  -> a -> Type
type Scoped1 a = forall nn. Vec a (Succ nn) -> a -> Type

data Elem :: Scoped1 a where
  EO :: Elem (x :> xs) x
  ES :: Elem xs x -> Elem (y :> xs) x
deriving instance 
  Show (Elem ctx ty)

data Exp :: Scoped Type where
  Var   :: Elem as a -> Exp as a
  Lam   :: Exp (a :> as) b -> Exp as (a -> b)
  App   :: Exp as (a -> b) -> (Exp as a -> Exp as b)
  Let   :: Exp as a -> Exp (a :> as) b -> Exp as b
  -- -- Arith :: Exp ctx Int -> ArithOp ty -> Exp ctx Int -> Exp ctx ty
  Cond  :: Exp as Bool -> Exp as a -> Exp as a -> Exp as a
  Fix   :: Exp as (a -> a) -> Exp as a
  IntE  :: Int  -> Exp as Int
  BoolE :: Bool -> Exp as Bool

deriving instance 
  Show (Exp ctx ty)

newtype Alg f a = Alg (f a -> a)

idAlg :: Alg Identity a
idAlg = Alg coerce

-- f   : f a -> a
-- g   : g a -> a
-- fga : f (g a)
compAlg :: forall f g a. Functor f => Alg f a -> Alg g a -> Alg (Compose f g) a
Alg f `compAlg` Alg g  = Alg $ \(Compose fga) -> 
  f (g <$> fga)

class Fls exp where fls :: exp Bool
class Tru exp where tru :: exp Bool
class Cnd exp where cnd :: exp Bool -> exp a -> exp a -> exp a
class Par exp where par :: exp a -> exp b -> exp (a, b)
class One exp where one :: exp (a, b) -> exp a
class Two exp where two :: exp (a, b) -> exp b

class TruTru exp where trutru :: exp (Bool, Bool) 

newtype Bld :: ((Type -> Type) -> Constraint) -> (Type -> Type) where
  Bld :: (forall xx. cls xx => xx a) -> Bld cls a

instance cls ~=> Tru => Tru (Bld cls) where
  tru :: Bld cls Bool
  tru = Bld (tru)

instance cls ~=> Fls => Fls (Bld cls) where
  fls :: Bld cls Bool
  fls = Bld (fls)

instance cls ~=> Cnd => Cnd (Bld cls) where
  cnd :: Bld cls Bool -> Bld cls a -> Bld cls a -> Bld cls a
  cnd (Bld cond) (Bld tru) (Bld fls) = Bld (cnd cond tru fls)

instance cls ~=> Par => Par (Bld cls) where 
  par :: Bld cls a -> Bld cls b -> Bld cls (a, b)
  par (Bld a) (Bld b) = Bld (par a b)
  
instance cls ~=> One => One (Bld cls) where 
  one :: Bld cls (a, b) -> Bld cls a
  one (Bld par) = Bld (one par)

instance cls ~=> Two => Two (Bld cls) where 
  two :: Bld cls (a, b) -> Bld cls b
  two (Bld par) = Bld (two par)

instance cls ~=> TruTru => TruTru (Bld cls) where 
  trutru :: Bld cls (Bool, Bool)
  trutru = Bld trutru

----------------------------------------------------------------------

newtype Overr :: ((Type -> Type) -> Constraint) -> (Type -> Type) where
  Overr :: (forall xx. cls xx => xx a) -> Overr cls a
  -- deriving 
  --   (One, Two)
  -- via 
  --   (Bld cls)

instance cls ~=> (Par & Tru) => TruTru (Overr cls) where
  trutru :: Overr cls (Bool, Bool)
  trutru = Overr (par tru tru)

instance cls ~=> (One & TruTru) => Tru (Overr cls) where
  tru :: Overr cls Bool
  tru = Overr (one trutru)

• tweet

Generalize stuff from generics-sop (currently reading http://staff.mmcs.sfedu.ru/~ulysses/Papers/2018-TFP-dgp-recursion.pdf)

data NP :: (a -> Type) -> ([a] -> Type) where
  Nil  :: NP f '[]
  (:*) :: f a -> NP f as -> NP f (a:as)

data NS :: (a -> Type) -> ([a] -> Type) where
  O :: f a     -> NS f (a:as)
  S :: NS f as -> NS f (a:as)

to vectors a la stitch, is this useful

-- natural numbers
data N = O | S N

-- length-indexed vectors
data Vec :: N -> Type -> Type where
  VNil :: Vec O a
  (:>) :: a -> Vec n a -> Vec (S n) a

-- n-ary products
data NP :: forall a n. (a -> Type) -> (Vec n a -> Type) where

  Nil  :: NP f VNil

  (:*) :: f a 
       -> NP f as
       -> NP f (a:>as)

-- n-ary sums
data NS :: forall a n. (a -> Type) -> (Vec (S n) a -> Type) where

  Here  :: f a     -> NS f (a:>as)
  There :: NS f as -> NS f (a:>as)

And sum-of-product gets kind

newtype SOP :: (a -> Type) -> (Vec (S n) (Vec m a) -> Type) where
  SOP :: NS (NP f) ass
      -> SOP f ass

Andres Löh points out that we probably don't want (S n) in the kind

Sorry, I only now see that S is in the kind of NS as well. I agree that that is probably not a good idea. You might still want to talk about an uninhabited NS f []

• tweet

class cls => Foo cls where
  wit :: Dict cls

instance Foo cls where
  wit :: Dict cls
  wit = ...

  Dict <- wit @cls

for use with things like (https://ghc.haskell.org/trac/ghc/ticket/14832, https://ghc.haskell.org/trac/ghc/ticket/14822)

class    Test (bool :: Bool)
instance Test False
instance Test True

class Test bool => Test' (bool :: Bool) where
  test' :: Dict (Test bool)

instance SingI bool => Test' bool where
  -- This provides the required `Test bool' constraint
  Dict <- test' @bool

  test' :: Dict (Test bool)
  test' = 
    case sing @_ @bool of
      SFalse -> Dict
      STrue  -> Dict

Have felt inspired by "Functional Pearl: Ghosts of Departed Proofs"

type Pi = Sing

class              IsNil (as :: [a])
instance           IsNil '[]
instance Bottom => IsNil (a:as)

class              IsCons (as :: [a])
instance Bottom => IsCons '[]
instance           IsCons (a:as)

classify :: Pi (as :: [a]) -> Either (Dict (IsNil as)) (Dict (IsCons as))
classify SNil    = Left  Dict
classify SCons{} = Right Dict

class              IsNil (as::[a])
instance           IsNil '[]
instance Bottom => IsNil (a:as)

class              IsCons (as::[a])
instance Bottom => IsCons '[]
instance           IsCons (a:as)

class              IsSing (as :: [a])
instance Bottom => IsSing '[]
instance           IsSing '[a]
instance Bottom => IsSing (a:b:bs)

class              LenTwoPlus (as :: [a])
instance Bottom => LenTwoPlus '[]
instance Bottom => LenTwoPlus '[a]
instance           LenTwoPlus (a:b:bs)

classify' 
  :: Pi (as :: [a]) 
  -> Dicts '[IsNil as, IsSing as, LenTwoPlus as]
classify' SNil              = Here
classify' (SCons _ SNil)    = Here & There
classify' (SCons a SCons{}) = Here & There & There

data Dicts :: [Constraint] -> Type where
  Here  :: cls => Dicts (cls:clss)
  There :: Dicts clss -> Dicts (cls:clss)

Using NS from generics-sop

data NS :: (k -> Type) -> ([k] -> Type) where
  Z :: f a     -> NS f (a:as)
  S :: NS f as -> NS f (a:as)

from we can replace Dicts = NS Dict

--   Dicts :: [Constraint] -> Type
type Dicts = NS Dict

classify' 
  :: Pi (as :: [a]) 
  -> Dicts '[IsNil as, IsSing as, LenTwoPlus as]
classify' SNil              = Dict & Z
classify' (SCons _ SNil)    = Dict & Z & S
classify' (SCons a SCons{}) = Dict & Z & S & S

Worth a shot

reflect_ :: forall s a. Reifies s a => a
reflect_ = reflect @s Proxy

-- reflect : (s ··> a) => (forall s -> a)

-- reify : a -> (forall name. (s ··> a) => forall s -> res) -> res

type (··>) = Reifies

newtype O a name = O a

instance name··>DOrd a => Eq (O a name) where
  (==) :: O a name -> O a name -> Bool
  a == b = compare a b == EQ
  
instance name··>DOrd a => Ord (O a name) where
  compare :: O a name -> O a name -> Ordering
  compare = coerce (reflect_ @name)

newtype DOrd a = DOrd (a -> a -> Ordering)
newtype DEq  a = DEq  (a -> a -> Bool)

ord_eq :: forall name a
        . (name··>DOrd a) 
       :- (name··>DEq  a)
ord_eq = Sub ord_eq' where

  ord_eq' :: name··>DOrd a => Dict (name ··> DEq a)
  ord_eq' = case reflect_ @name of
    DOrd cmp -> let

      eq :: DEq a
      eq = DEq (\a b -> cmp a b == EQ)

      in reify eq (\p -> Dict)

• tweet

newtype Named (name :: Type) a = Named a

instance The (Named name a) a

type a~~name = Named name a

(~~) :: forall a res. a -> (forall (xx::Type). a~~xx -> res) -> res
(~~) = flip coerce

name :: forall name a. a -> a~~name
name = Named

axiom :: forall cls name. Dict (cls name)
axiom = unsafeCoerce (Dict :: Dict ())

class IsNil  (name::k)
class IsCons (name::k)

classify :: [a]~~name -> Dict (IsNil name) + Dict (IsCons name)
classify = \case
  The [] -> Left  axiom
  The _  -> Right axiom

head_ :: IsCons name => [a]~~name -> a
head_ = uncons >>> fst

tail_ :: IsCons name => [a]~~name -> [a]
tail_ = uncons >>> snd

uncons :: IsCons name => [a]~~name -> (a, [a])
uncons = the >>> \case
  []   -> error "The 'IsCons name' constraint makes this illegal."
  a:as -> (a, as)

{-# Complete NIL, CONS #-}
pattern NIL :: () => IsNil name => [a]~~name
pattern NIL <- (classify -> Left Dict)

getCons :: [a]~~name -> Maybe (Dict (IsCons name), (a, [a]))
getCons as = 
  case classify as of
    Left{}     -> Nothing
    Right Dict -> Just (Dict, uncons as)

pattern CONS :: () => IsCons name => a -> [a] -> [a]~~name
pattern CONS a as <- (getCons -> Just (Dict, (a, as)))

Implementing reflection being precise about what we assume (Coercion (Galdur a res) (New a res))

class Taka (nafn :: Type) a | nafn -> a where
  taka :: Ty nafn -> a

data Ty (nafn :: Type) = Ty 

newtype Galdur a res = Galdur (forall nafn. Taka nafn a    => (Ty nafn -> res))
newtype New    a res = New    (forall nafn. (Ty nafn -> a) -> (Ty nafn -> res))

gefa :: forall a res. a -> (forall name. Taka name a => Ty name -> res) -> res
gefa a cont | let

  axiom :: Coercion (Galdur a res) (New a res)
  axiom = unsafeCoerce (Coercion :: forall a. Coercion a a)

  galdur :: Galdur a res
  galdur = Galdur cont

  new :: New a res
  new = coerceWith axiom galdur,

  New res <- new

  = res (\_ -> a) Ty

Implementation of https://forum.azimuthproject.org/discussion/2213/lecture-38-chapter-3-databases/p1

type Grph node = node -> node -> Type

data Node = Employee | Department | Str

data Work :: Grph Node where
  Manager   :: Work Employee   Employee
  WorksIn   :: Work Employee   Department
  Secretary :: Work Department Employee 
  FirstName :: Work Employee   Str
  DepName   :: Work Department Str

data Empl = Empl
  { name    :: String
  , manager :: Empl
  , dep     :: Dep
  }

data Dep = Dep
  { depName   :: String
  , secretary :: Empl
  }

type family
  El (node :: Node) = (res :: Type) | res -> node where
  El Employee   = Empl
  El Department = Dep
  El Str        = String

varp :: Work a b -> (El a -> El b)
varp = \case
  Manager -> 
    manager

  WorksIn -> 
    dep

  Secretary -> 
    secretary

  FirstName -> 
    name

  DepName -> 
    depName

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