Last active
October 15, 2018 20:46
-
-
Save Icelandjack/cfa3d5820aaf880b6ec918d96ee3e6ac to your computer and use it in GitHub Desktop.
For Chris Allen, braindump
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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 |
-- 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)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
(Binary) Product categories are basically the product of two categories. Any two functions
can be written as a single arrow in the product category
(->) × (->)
Defining coproducts as an adjunction makes use of product categories, the functors go from product categories
It is used in the adjunction defining
But what about a generalization for 0-, 1-, 2-, ... product categories? With this prelude:
We go on to define the first attempt:
This only allows for
(->)
functionsThe first and last type-level lists should always have the same length:
But we really want to allow for different categories, of different kinds? So one arrow might be between
Nat
objectswhich allows different kinds