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 .

For example the Haskell expression

\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:

**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).

[License] : https://en.wikipedia.org/wiki/BSD_licenses#3-clause_license_(%22BSD_License_2.0%22,_%22Revised_BSD_License%22,_%22New_BSD_License%22,_or_%22Modified_BSD_License%22)

*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

add = 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 ()

For example the Haskell expression

\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).

[License] : https://en.wikipedia.org/wiki/BSD_licenses#3-clause_license_(%22BSD_License_2.0%22,_%22Revised_BSD_License%22,_%22New_BSD_License%22,_or_%22Modified_BSD_License%22)