tagless encoding of mutually recursive types

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?

---

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

The type forall proc. ProcSYM proc => proc Int forall proc. ProcSYM proc => proc Int (the type of myProc ) on the other hand, promises, no matter how you construct proc s, 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.")

链接地址: http://www.djcxy.com/p/87348.html

上一篇: 在MVC 6中调整上传的图像大小

下一篇: 相互递归类型的无标记编码