-
-
Save Icelandjack/cfa3d5820aaf880b6ec918d96ee3e6ac to your computer and use it in GitHub Desktop.
-- 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 |
Icelandjack
commented
Jul 12, 2018
- tweet
-- · 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)