Final-tagless encoding of mutually recursive types

Question

I am trying to express a pair of mutually recursive data types in the final-tagless encoding.

I am able to write:

{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ExplicitForAll #-}
module Test where

  class ExprSYM repr where
    expr :: forall proc. (ProcSYM proc) => proc Int -> repr

  class ProcSYM repr where
    varProc :: forall a. String -> repr a
    intProc :: String -> repr Int
    subjectOf :: forall expr. (ExprSYM expr) => expr -> repr Int

  myProc = intProc "proc A."

However, when I write:

myExpr = expr myProc

I receive the following error:

Could not deduce (Test.ProcSYM proc0)
  arising from a use of ‘Test.expr’
from the context (Test.ExprSYM repr)
  bound by the inferred type of
           Test.myExpr :: Test.ExprSYM repr => repr
  at src/Test.hs:16:3-22
The type variable ‘proc0’ is ambiguous
In the expression: Test.expr Test.myProc
In an equation for ‘Test.myExpr’:
    Test.myExpr = Test.expr Test.myProc

Does any such encoding require the use of functional dependencies (or equivalent) to expess the constraint between the two representation types?

If so, how would I write this?

Answer 1

Let's start by looking at the type of myProc

myProc :: ProcSYM repr => repr Int
myProc = intProc "proc A."

This says, forall types repr where ProcSYM repr, I'm a value of type repr Int. If we had multiple implementations of ProcSYM, this is a value that's polymorphic in all of them. For example, if we had a corresponding tagged GADT ProcSYM' with a ProcSYM instance, myProc could be used as a value of ProcSYM'.

{-# LANGUAGE GADTs #-}

data ProcSYM' a where
    VarProc :: String -> ProcSYM' a
    IntProc :: String -> ProcSYM' a

instance ProcSYM ProcSYM' where
    varProc = VarProc
    intProc = IntProc

myProc' :: ProcSYM' Int
myProc' = myProc

The ProcSym repr constraint in myProc :: ProcSYM repr => repr Int is providing a way to construct reprs, which is exactly what myProc does. No matter which ProcSym repr you want, it can construct a repr Int.

The ProcSYM proc constraint in the type of expr :: forall proc. (ProcSYM proc) => proc Int -> repr is kind of meaningless. The constraint ProcSYM proc is once again providing a means to construct procs. It can't help us look inside or deconstruct a proc Int. Without a way to look inside proc Ints, we might as well not have the proc Int argument and instead read expr :: repr.

The type forall proc. ProcSYM proc => proc Int (the type of myProc) on the other hand, promises, no matter how you construct procs, I can provide a value of that type. You want to pass myProc as the first argument to expr, as evidenced by

myExpr = expr myProc

Passing in a polymorphic value of this type without choosing a concrete proc requires RankNTypes.

class ExprSYM repr where
    expr :: (forall proc. ProcSYM proc => proc Int) -> repr

The instance for ExprSYM can choose the ProcSYM dictionary to pass into the first argument. This allows the implementation of expr to deconstruct the proc Int. We'll demonstrate this by completing an example with GADTs to see what this is doing. We will also make the same change to the type of subjectOf.

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
module Test where

class ExprSYM repr where
    expr :: (forall proc. ProcSYM proc => proc Int) -> repr

class ProcSYM repr where
    varProc :: forall a. String -> repr a
    intProc :: String -> repr Int
    subjectOf :: (forall expr. ExprSYM expr => expr) -> repr Int

-- Tagged representation for ExprSYM
data ExprSYM' where
    Expr :: ProcSYM' Int -> ExprSYM'
deriving instance Show ExprSYM'

instance ExprSYM ExprSYM' where
    expr x = Expr x  -- chooses that the ProcSYM proc => proc Int must be ProcSYM' Int

-- Tagged representation for ProcSYM
data ProcSYM' a where
    VarProc :: String -> ProcSYM' a
    IntProc :: String -> ProcSYM' a
    SubjectOf :: ExprSYM' -> ProcSYM' Int

deriving instance Show (ProcSYM' a)

instance ProcSYM ProcSYM' where
    varProc = VarProc
    intProc = IntProc
    subjectOf x = SubjectOf x  -- chooses that the ExprSYM repr => repr must be ExprSYM'

-- myProc and myExpr with explicit type signatures
myProc :: ProcSYM repr => repr Int
myProc = intProc "proc A."

myExpr :: ExprSYM repr => repr
myExpr = expr myProc

main = print (myExpr :: ExprSYM')

This outputs an abstract syntax tree for myExpr. We can see that if the implementation of expr wanted to deconstruct the ProcSYM proc => proc Int value it could (and in this case did) provide a ProcSYM dictionary that builds values it knows how to deconstruct. We can see this in the IntProc constructor in the shown value.

Expr (IntProc "proc A.")