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 |
Author
Icelandjack
commented
Aug 27, 2018
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