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 piggy-back 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/de-typechecker.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 if-then-else 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

1 |
(a~Something) => MyClass 'True a |

rather than

1 |
Myclass 'True Something |

The type inference tends to be better.

Here are some usage examples of toCcc.

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 |
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 constrained-categories package?

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 |
{-# 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

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 |
{-# 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 -} |