Hi [Matthew](https://forum.azimuthproject.org/profile/1818/Matthew%20Doty), I've been working on your [Puzzle3](https://forum.azimuthproject.org/discussion/comment/16735/#Comment_16735) and I'm stuck with the last twi pieces: `run` and `interpret`.

My code from Conal's paper is this:

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}

module CompilingToCategories where

import Prelude hiding (it, (.), curry, uncurry, const)

-- Classes

infixr 9 .
class Category k where
id :: a `k` a
(.) :: (b `k` c) -> (a `k` b) -> (a `k` c)

infixr 3 |*|
class Category k => Cartesian k where
(|*|) :: (a `k` c) -> (a `k` d) -> (a `k` (c, d))
exl :: (a, b) `k` a
exr :: (a, b) `k` b

-- How to generalize () for any category?
class Category k => Terminal k where
it :: a `k` ()

class Cartesian k => Closed k where
applyC :: ((a -> b), a) `k` b
curry :: ((a, b) `k` c) -> (a `k` (b -> c))
uncurry :: (a `k` (b -> c)) -> ((a, b) `k` c)

class Terminal k => ConstCat k b where
unitArrow :: b -> (() `k` b)

const :: ConstCat k b => b -> (a `k` b)
const b = unitArrow b . it

class Cartesian k => BoolCat k where
notC :: Bool `k` Bool
andC, orC :: (Bool, Bool) `k` Bool
ifteC :: (Bool, (a, a)) `k` a

class NumCat k a where
negateC :: a `k` a
addC, mulC :: (a, a) `k` a

class OrdCat k a where
gteC :: (a, a) `k` Bool

-- Instances

instance Category (->) where
id = \x -> x
g . f = \x -> g (f x)

instance Cartesian (->) where
f |*| g = \x -> (f x, g x)
exl = \(a, b) -> a
exr = \(a, b) -> b

instance Terminal (->) where
it = \a -> ()

instance Closed (->) where
applyC (f, a) = f a
curry f = \a b -> f (a, b)
uncurry f = \(a, b) -> f a b

instance ConstCat (->) b where
unitArrow b = \() -> b

instance BoolCat (->) where
notC = not
andC = uncurry (&&)
orC = uncurry (||)
ifteC = \(b, (t, e)) -> if b then t else e

instance Num a => NumCat (->) a where
negateC = negate
addC = uncurry (+)
mulC = uncurry (*)

instance Ord a => OrdCat (->) a where
gteC = uncurry (>=)

And my implementation for `Language` and `Interpreted` is:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module LanguageCat where

import Prelude hiding (it, (.), curry, uncurry, const)

import CompilingToCategories
import Language

-- In the code below
-- find a concrete value for `l`
-- and elide all the mocks

swap :: Cartesian k => (a, b) `k` (b, a)
swap = exr |*| exl

instance (Closed k
,ConstCat k Int, NumCat k Int, OrdCat k Int
,ConstCat k Bool, BoolCat k
) => Language k where
here = exl
before f = f . exr
lambda f = curry (f . swap)
apply f g = applyC . (f |*| g)

loop f = applyC . ( f |*| loop f)

int = const
add a b = addC . (a |*| b)
mult a b = mulC . (a |*| b)
down a = add a (int (-1))
up a = add a (int 1)
gte a b = gteC . (a |*| b)

bool = const
and a b = andC . (a |*| b)
or a b = orC . (a |*| b)
neg a = notC . a

ifte b t e = ifteC . (b |*| t |*| e)

instance (Closed k
,ConstCat k Int, NumCat k Int, OrdCat k Int
,ConstCat k Bool, BoolCat k)
=> Interpreted k where
run = undefined

--interpret :: Term a -> a
--interpret t = (run :: h `l` a -> h -> a) t ()

It compiles, but althougth this is Haskell, maybe there are some errors :-D

Any ideas, hints, comments to advance further in the Puzzle?

Thanks !!!