Approximating Compiling to Categories using Typelevel Haskell: Take 2
The previous episode is here .
Summary: I’m trying to use typelevel programming in Haskell to achieve some of the aims of Conal Elliott’s compiling to categories GHC plugin. The types of highly polymorphic tuple functions are enough to specify the implementation. We aren’t going to be able to piggyback off of GHC optimizations (a huge downside), but we can reify lambdas into other categories and avoid the scariness of plugins.
The current implementation github source is here
JESUS CHRIST.
http://okmij.org/ftp/Haskell/detypechecker.lhs
Of course, Oleg already did it. This is a file where he builds the implementation of a polymorphic function from the type signature. Instead of tuples, he is focusing on higher order functions with deep nesting of (>).
The trick that I was missing is in the IsFunction typeclass at the very end, which is only achievable as a Incoherent instances.
I would never have had the courage to use an Incoherent instance if I hadn’t seen a higher authority do it first. It has turned out in my typelevel journey that many instances that I’ve been tempted to make overlapping or incoherent don’t actually have to be, especially with the availability of closed type families. I think you really do need Incoherent in this application because type variables stay polymorphic forever.
To the best of my knowledge, if you need to differentiate between a tuple type (a,b) and an uninstantiated polymorphic value a’ like we do when deconstructing the input type of our lambda, you need to use an Incoherent instance. Since a’ could hypothetically eventually be unified to some (a,b) we should not be able to do different things for the two cases without stepping outside the usual laws of typeclass resolution.
New features of the implementation:

The new implementation does not require the V annotation of the input like previous version by using the previously mentioned. This is super cool because now I can throw the stock Prelude.fst into toCcc.

I changed how the categorical implementation is built, such that it short circuits with an ‘id’ if a large structure is needed from the input, rather than deconstructing all the way to every piece of the input. Lots of other optimizations would be nice (vital?), but it is a start.

I also implemented a FreeCat GADT so that we can see the implementation in ghci.

I switched from using Data.Proxy to the type annotations extensions, which is a huge readability win.

I added a binary application operator binApp, which is useful for encapsulating categorical literals as infix operators into your lambda expressions.

General cleanup, renaming, and refactoring into library files.
A couple typelevel tricks and comments:
You often have to make helper typeclasses, so don’t be afraid to. If you want something like an ifthenelse in your recursion, it is very likely you need a form of the typeclass that has slots for ‘True or ‘False to help you pick the instance.
If possible, you often want the form
(a~Something) => MyClass 'True a
rather than
Myclass 'True Something
The type inference tends to be better.
Here are some usage examples of toCcc.
example6 = toCcc (\x > x) 'a'
example7 = toCcc @FreeCat (\(x, y) > x)
example8 = toCcc @FreeCat (\(x, y) > y)
example8andahalf = toCcc' (Proxy :: Proxy FreeCat) (\(x, y) > y)
example9 = toCcc @FreeCat (\(x, y) > (y,x))
example10 = toCcc @FreeCat (\(( x, z), y) > (y,x))
swappo = toCcc @FreeCat $ \((x, z), y) > (x,(z,y))
example11 = toCcc @(>) $ \(x,y) > binApp addC x y
example12 = toCcc @(>) $ \(x,y) > App negateC x
 infix synonyms
(+++) = binApp addC
(***) = binApp mulC
example13 = toCcc @(>) $ \(x,(y,z)) > x +++ (y *** z)
My partially implemented version of some of Conal’s category typeclasses. Should I switch over to using the constrainedcategories package?
{# LANGUAGE GADTs, StandaloneDeriving, NoImplicitPrelude #}
module Cat where
import Control.Category
import Prelude hiding ((.))
class Category k => Monoidal k where
par :: k a c > k b d > k (a,b) (c,d)
class Monoidal k => Cartesian k where
fst :: k (a,b) a
snd :: k (a,b) b
dup :: k a (a,a)
fan f g = (par f g) . dup
data FreeCat a b where
Comp :: FreeCat b c > FreeCat a b > FreeCat a c
Id :: FreeCat a a
Fst :: FreeCat (a,b) a
Snd :: FreeCat (a,b) b
Dup :: FreeCat a (a,a)
Par :: FreeCat a b > FreeCat c d > FreeCat (a,c) (b,d)
deriving instance Show (FreeCat a b)
instance Category FreeCat where
(.) = Comp
id = Id
instance Monoidal FreeCat where
par = Par
instance Cartesian FreeCat where
fst = Fst
snd = Snd
dup = Dup
instance Monoidal (>) where
par f g = \(x,y) > (f x, g y)
instance Cartesian (>) where
fst (x,y) = x
snd (x,y) = y
dup x = (x,x)
class NumCat k where
mulC :: Num a => k (a,a) a
negateC :: Num a => k a a
addC :: Num a => k (a,a) a
instance NumCat (>) where
mulC = uncurry (*)
negateC = negate
addC = uncurry (+)
The actual implementation of toCcc
{# LANGUAGE DataKinds,
AllowAmbiguousTypes,
TypeFamilies,
TypeOperators,
MultiParamTypeClasses,
FunctionalDependencies,
PolyKinds,
FlexibleInstances,
UndecidableInstances,
TypeApplications,
NoImplicitPrelude,
ScopedTypeVariables #}
module CCC (
CCC
, App (App)
, binApp
, toCcc'
, toCcc ) where
import Cat
import Data.Proxy
import Data.Type.Equality (type (==))
import Prelude (Bool(..))
import Control.Category
 The unfortunate Incoherent instances I need to force polymorphic values
class IsTup a b  a > b
instance {# INCOHERENT #} (c ~ 'True) => IsTup (a,b) c
instance {# INCOHERENT #} (b ~ 'False) => IsTup a b
data Leaf n = Leaf
data Z
data S a
data App f a = App f a
f $$ x = App f x
binApp f a b = App f (a,b)
class Cartesian k => CCC k a a' b'  a a' > b' where
toCcc :: a > k a' b'
instance (Tag a,
Build k a b a' b',
Cartesian k)
=> CCC k (a>b) a' b' where
toCcc f = build @k @a @b @a' @b' res where  build (Proxy :: Proxy labels) (Proxy :: Proxy b) res where
res = f val
toCcc' :: CCC k f a' b' => Proxy k > f > k a' b'
toCcc' _ f = toCcc f
class Tag a where
val :: a
instance (IsTup a flag, Tag' a Z flag n) => Tag a where
val = val' @a @Z @flag
class Tag' a n (flag :: Bool) n' a n flag > n' where
val' :: a
instance (IsTup a flaga,
IsTup b flagb,
Tag' a n flaga n'',
Tag' b n'' flagb n') => Tag' (a,b) n 'True n' where
val' = (val' @a @n @flaga, val' @b @n'' @flagb)
instance (a ~ Leaf n) => Tag' a n 'False (S n) where
val' = Leaf
type family Or a b where
Or 'True b = 'True
Or a 'True = 'True
Or 'False 'False = 'False
class In a b flag  a b > flag where
instance (
((a,b) == c) ~ isc,
flag' ~ Or flaga flagb,
flag ~ Or flag' isc,
In a c flaga,
In b c flagb) => In (a,b) c flag
instance ((Leaf n == c) ~ flag) => In (Leaf n) c flag
class Build k input key a' b'  input key a' > b' where
build :: Cartesian k => key > k a' b'
instance (
iseq ~ ((a,b) == key),
In a key isinleft,
In b key isinright,
Cond k iseq isinleft isinright (a,b) key a' b'
) => Build k (a,b) key a' b' where
build key = cond @k @iseq @isinleft @isinright @(a,b) @key @a' key
instance (Leaf n ~ b, a' ~ b') => Build k (Leaf n) b a' b' where
build _ = id
class Cond k iseq isinleft isinright input key a b  iseq isinleft isinright input key a > b where
cond :: Cartesian k => key > k a b
 Find the key is in the input
instance (a ~ b) => Cond k 'True x x input key a b where
cond _ = id
instance (Build k a key a' c', (a',b') ~ ab) => Cond k 'False 'True x (a,b) key ab c' where  get those input types inferred baby!
cond key = (build @k @a @key @a' key) . fst
instance (Build k b key b' c', (a',b') ~ ab) => Cond k 'False 'False 'True (a,b) key ab c' where
cond key = (build @k @b @key @b' key) . snd
 Otherwise destruct on the key
instance (Build k input key1 a' c',
Build k input key2 a' d') => Cond k 'False 'False 'False input (key1,key2) a' (c',d') where
cond (key1,key2) = fan (build @k @input @key1 @a' key1) (build @k @input @key2 @a' key2)
instance (Build k input key a' b',
f ~ k b' c')
=> Cond k 'False 'False 'False input (App f key) a' c' where
cond (App f key) = f . (build @k @input @key @a' key)
 Could I replace almost everything with App? A very powerful construct
 This is a of some relation to defunctionalization like in HList
 Maybe I should build a typelevel FreeCat and then do compilation passes on it
{
type family (StripLeaf a) where
StripLeaf (a,b) = (StripLeaf a, StripLeaf b)
StripLeaf (Leaf n a) = a
}