A lot of people are excited about Conal Elliot's paper [Compiling to Categories (2017)](http://conal.net/papers/compiling-to-categories/). So I was thinking of adapting an exercise I know so we can start to understand it together.

*Finally tagless* DSLs are a style of specifying small languages in Haskell, Agda and Coq using type classes. They were first introduce by Carette, Kiselyov and Shan in [*Finally Tagless, Partially Evaluated*](http://okmij.org/ftp/tagless-final/JFP.pdf). A real world example of an application of this approach is the [servant library](https://github.com/haskell-servant/servant) for building web applications in Haskell.

What is flexible about finally tagless DSLs is that because the language is defined in a type class and the semantics are defined in a instance implementation.

My goal is to write a finally tagless DSL and ultimately write an instance implementation for it using the classes Conal Elliot introduces in §2 of his paper.

The following is adapted from Joseph Abrahamson, who originally published this exercise on [Code Wars](https://www.codewars.com). It is open source under the [BSD2 license][License].

This simple finally tagless DSL uses De Bruijn indices for encoding \$$\lambda\$$-expressions in the simply typed \$$\lambda\$$-calculus. It also includes a fixed point operation for encoding recursion as well as integers and .


{-# LANGUAGE Rank2Types          #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- After getting rid of mocks, shouldn't need these two below
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE MonoLocalBinds      #-}

module Tagless where

import Prelude hiding (and, or)

class Language k where
here   :: (a, h) k a
before :: h k a -> (any, h) k a
lambda :: (a, h) k b -> h k (a -> b)
apply  :: h k (a -> b) -> (h k a -> h k b)

loop   :: h k (a -> a) -> h k a

int    :: Int -> h k Int
add    :: h k Int -> h k Int -> h k Int
down   :: h k Int -> h k Int
up     :: h k Int -> h k Int
mult   :: h k Int -> h k Int -> h k Int
gte    :: h k Int -> h k Int -> h k Bool

bool   :: Bool -> h k Bool
and    :: h k Bool -> h k Bool -> h k Bool
or     :: h k Bool -> h k Bool -> h k Bool
neg    :: h k Bool -> h k Bool

ifte   :: h k Bool -> h k a -> h k a -> h k a

class Language k => Interpreted k where
run :: h k a -> h -> a

type Term a = forall k h . Language k => h k a

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

instance Language l where
here   = undefined
before = undefined
lambda = undefined
apply  = undefined

loop   = undefined

int    = undefined
mult   = undefined
down   = undefined
up     = undefined
gte    = undefined

bool   = undefined
and    = undefined
or     = undefined
neg    = undefined

ifte   = undefined

instance Interpreted l where
run = undefined

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


\a -> \b -> a + b

would be expressed as a Term in this DSL with

ex :: Term (Int -> Int -> Int)
ex = lambda (lambda (add (before here) here))

**Finally Tagless Puzzle 1**: Write an instance for this language.

Here are some test vectors:


interpret (apply (lambda here) (int 6)) == 6



interpret (apply (lambda here) (bool True)) == True



interpret (ifte (bool True) (int 3) (int 4)) == 3


**Finally Tagless Puzzle 2**: Write an instance for this language without using newtype or data, just base

**Finally Tagless Puzzle 3**: Use the various category type classes that Conal Elliot introduces to make an abstract instance for this DSL (I have not yet managed this exercise myself, but you will need NumCat and BoolCat at least).

If you are working this out, it doesn't hurt to read [Oleg Kiselyov's lecture notes](http://okmij.org/ftp/tagless-final/course/lecture.pdf) or watch [Joseph Abrahamson's talk](https://www.youtube.com/watch?v=JxC1ExlLjgw).