So I’ve been trying to try and approximate Conal Elliott’s compiling to categories in bog standard Haskell and I think I’ve got an interesting chunk.

His approach in using a GHC plugin is better for a couple reasons. One really important thing is that he gets to piggy back on GHC optimizations for the lambdas. I have only implemented a very bad evaluation strategy. Perhaps we could recognize shared subexpressions and stuff, but it is more work. I seem somewhat restricted in what I can do and sometimes type inference needs some help. Not great. However, GHC plugins definitely bring their own difficulties.

What I’ve got I think still has roots in my thinking from this previous post

There are a couple insights that power this implementation

- A fully polymorphic tuple to tuple converter function is uniquely defined by it’s type. For example, swap :: (a,b) -> (b,a), id:: a -> a, fst :: (a,b) ->a, snd::(a,b)->b are all unique functions due to the restrictions of polymorphism. Thus typelevel programming can build the implementation from the type.
- Getting a typeclass definition to notice polymorphism is hard though. I haven’t figured out how to do it, if it is even possible. We get around it by explicitly newtyping every pattern match on a polymorphic variable like so \(V x, V y) -> (y,x). Two extra characters per variable. Not too shabby.
- You can abuse the type unification system as a substitution mechanism. Similar to HOAS, you can make a lambda interpreter at the type level that uses polymorphism as way of generating labels for variables. This is probably related to Oleg Kiselyov’s type level lambda calculus, but his kind of confuses me http://okmij.org/ftp/Computation/lambda-calc.html#haskell-type-level
- You can inject a categorical literal morphism using a wrapping type to be extracted later using an apply operator and type App f a. An infix ($$) makes it feel better.

1 2 3 4 5 6 7 8 9 10 |
class Eval e r | e -> r data App f b newtype V a = V a type Lit a = V a type Lam a b = a -> b -- Let's borrow arrow for Lambda instance (Eval b d, a ~ c) => Eval (App (a -> b) c) d instance (Eval b c) => Eval (a -> b) (a -> c) -- Evaluate inside the body or stop? instance Eval (Lit a) (Lit a) |

So here is the rough structure of what the typelevel programming is doing

You can do a depth first traversal of the input tuple structure, when you hit V, unify the interior type with a Nat labelled Leaf. At the same time, you can build up the actual value of the structure so that you can apply the lambda to it and get the output which will hold a tree that has morphism literals you want.

Then inspect the output type of the lambda which now has Nat labels, and traverse the labelled tree again to find the appropriate sequence of fst and snd to extract what you need. If you run into an application App, you can pull the literal out now and continue traversing down.

At the moment I’ve only tested with the (->) Category, which is a bit like demonstrating a teleporter by deconstructing a guy and putting back in the same place, but I think it will work with others. We’ll see. I see no reason why not.

At the moment, I’m having trouble getting GHC to not freakout unless you explicitly state what category you’re working in, or explicitly state that you’re polymorphic in the Category k.

Some future work thoughts: My typelevel code is complete awful spaghetti written like I’m a spastic trapped animal. It needs some pruning. I think all those uses of Proxy can be cleaned up by using TypeApplications. I need to implement some more categories. Should I conform to the Constrained-Categories package? Could I use some kind of hash consing to find shared structures? Could Generic or Generic1 help us autoplace V or locate polymorphism? Maybe a little Template Haskell spice to inject V?

Here’s the most relevant bits, with my WIP git repository here

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 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 |
{-# LANGUAGE FunctionalDependencies, FlexibleInstances, GADTs, DataKinds, TypeOperators, KindSignatures, PolyKinds, FlexibleContexts, UndecidableInstances, ScopedTypeVariables, NoImplicitPrelude #-} module Main where import Lib import GHC.TypeLits import Data.Proxy import Prelude hiding (id, fst, snd, (.)) main :: IO () main = someFunc -- We will use these wrappers to know when we've hit polymorphism newtype V a = V a data Z data S a data Leaf n a = Leaf data Node n a b = Node a b ccc' :: Top a b c k => Proxy k -> a -> k b c ccc' _ f = ccc f class Tag a b c d mono | a b mono -> d c where val :: Proxy a -> Proxy b -> Proxy mono -> a instance (Tag a n n'' r1 a', Tag b n'' n' r2 b', (a', b') ~ q) => Tag (a, b) n n' (Node n'' r1 r2) q where val _ _ _ = (val (Proxy :: Proxy a) (Proxy :: Proxy n) (Proxy :: Proxy a'), val (Proxy :: Proxy b) (Proxy :: Proxy n'') (Proxy :: Proxy b')) instance (a ~ Leaf n a') => Tag (V a) n (S n) (Leaf n a') a' where val _ _ _ = V Leaf class CartesianCategory k => Top a b c k | a b -> c where ccc :: a -> k b c instance (Tag a Z n labels c, Build labels b c d k, CartesianCategory k) => Top (a->b) c d k where ccc f = build (Proxy :: Proxy labels) (Proxy :: Proxy b) res where res = f (val (Proxy :: Proxy a) (Proxy :: Proxy Z) (Proxy :: Proxy c)) fan f g = (par f g) . dup -- Once you've labelled, traverse the output type and extract those pieces -- and put them together class CartesianCategory k => Build labels b c d k | labels b -> c d where build :: Proxy labels -> Proxy b -> b -> k c d instance (Build labels b i o1 k, Build labels c i o2 k) => Build labels (b,c) i (o1,o2) k where build pl pbc (x,y) = fan (build pl (Proxy :: Proxy b) x) (build pl (Proxy :: Proxy c) y) instance (Extract labels n a b, CartesianCategory k) => Build labels (Leaf n c) a b k where build pl pb _ = extract pl (Proxy :: Proxy n) instance (Build labels c a b k, CartesianCategory k) => Build labels (App (k b d) c) a d k where build pl pb (App f x) = f . (build pl (Proxy :: Proxy c) x) class StripN a b | a -> b instance (StripN a a', StripN b b') => StripN (Node n a b) (a',b') instance StripN (Leaf n a) a -- Builds the extractor function class Extract a n d r | a n -> d r where extract :: CartesianCategory k => Proxy a -> Proxy n -> k d r instance (LT n n' gt, -- which one is greater StripN (Node n' a b) ab, FstSnd gt ab r1, -- get value level rep of this ITE gt a b c, -- Select to go down branch Extract c n r1 r) -- recurse => Extract (Node n' a b) n ab r where extract _ p = (extract (Proxy :: Proxy c) p) . (fstsnd (Proxy :: Proxy gt)) instance Extract (Leaf n a) n a a where extract _ _ = id arrccc :: (Top a b c (->)) => a -> b -> c arrccc = ccc' (Proxy :: Proxy (->)) -- applying the category let's us imply arrow example6 = ccc (\(V x) -> x) 'a' --example7 :: CartesianCategory k => k _ _ example7 = arrccc (\(V x, V y) -> x) -- ('a','b') example8 = arrccc (\(V x, V y) -> y) -- ('a','b') example9 = arrccc (\(V x, V y) -> (y,x)) -- ('a','b') example10 = arrccc (\((V x,V z), V y) -> (y,x)) -- ((1,'b'),'c') swappo = arrccc $ \((V x,V z), V y) -> (x,(z,y)) class FstSnd a d r | a d -> r where fstsnd :: CartesianCategory k => Proxy a -> k d r instance FstSnd 'True (a,b) a where fstsnd _ = fst instance FstSnd 'False (a,b) b where fstsnd _ = snd class Fst a b | a -> b instance Fst (a,b) a class Snd a b | a -> b instance Snd (a,b) b class ITE a b c d | a b c -> d instance ITE 'True a b a instance ITE 'False a b b class GT a b c | a b -> c instance GT a b d => GT (S a) (S b) d instance GT Z (S a) 'False instance GT (S a) Z 'True instance GT Z Z 'False class LT a b c | a b -> c instance LT a b d => LT (S a) (S b) d instance LT Z (S a) 'True instance LT (S a) Z 'False instance LT Z Z 'False -- For external function application data App f a = App f a f $$ x = App f x plus :: (Int, Int) -> Int plus (x,y) = x + y plus' (x,y) = x + y inc :: Int -> Int inc = (+ 1) --example11 = ccc (\(x,y) -> App plus (x,y)) example11 = arrccc (\(V x) -> App inc x) -- $ (1 :: Int) example12 = arrccc (\(V x,V y) -> plus $$ (x,y)) example13 = arrccc (\(V x,V y) -> inc $$ (plus $$ (x,y))) example14 :: Num a => (a,a) -> a -- Without this annotation it inferred Integer? Monomorphization? example14 = ccc (\(V x,V y) -> plus' $$ (x,y)) class CartesianCategory k where (.) :: k b c -> k a b -> k a c id :: k a a fst :: k (a,b) a snd :: k (a,b) b dup :: k a (a,a) par :: k a c -> k b d -> k (a,b) (c,d) instance CartesianCategory (->) where id = \x -> x fst (x,y) = x snd (x,y) = y dup x =(x,x) f . g = \x -> f (g x) par f g = \(x,y) -> (f x, g y) |

## 2 thoughts on “Shit Compiling to Categories using Type level Programming in Haskell”