相互递归类型的无标记编码
我试图在final-tagless编码中表达一对相互递归的数据类型。
我可以写：
{-# 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."
但是，当我写：
myExpr = expr myProc
我收到以下错误：
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
任何这样的编码是否需要使用函数依赖关系（或等价物）来处理两种representation类型之间的约束？
如果是这样，我会如何写这个？
我们先看看myProc的类型
myProc :: ProcSYM repr => repr Int
myProc = intProc "proc A."
这是说， forall类型repr其中ProcSYM repr ，我是类型的值repr Int 。 如果我们有多个ProcSYM实现，这是一个在所有这些实现中都是多态的值。 例如，如果我们有一个带有ProcSYM实例的相应标签GADT ProcSYM' ， myProc可以使用myProc作为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
ProcSym repr约束在myProc :: ProcSYM repr => repr Int中提供了一种构建repr的方法，这正是myProc所做的。 无论您需要哪个ProcSym repr ，都可以构建repr Int 。
expr :: forall proc. (ProcSYM proc) => proc Int -> repr类型中的ProcSYM proc约束expr :: forall proc. (ProcSYM proc) => proc Int -> repr expr :: forall proc. (ProcSYM proc) => proc Int -> repr是没有意义的。 约束ProcSYM proc再次提供构建一个手段proc秒。 它无法帮助我们查看内部或解构一个proc Int 。 如果没有办法查看proc Int ，我们可能不会有proc Int参数，而是读取expr :: repr 。
类型所有过程forall proc. ProcSYM proc => proc Int forall proc. ProcSYM proc => proc Int （类型myProc ），另一方面，承诺，无论你如何构建proc S，我可以提供这种类型的值。 您希望将myProc作为第一个参数传递给expr ，如所证明的
myExpr = expr myProc
传递此类型的多态值而不选择具体的proc需要RankNTypes 。
class ExprSYM repr where
expr :: (forall proc. ProcSYM proc => proc Int) -> repr
ExprSYM的实例可以选择ProcSYM字典传入第一个参数。 这允许执行expr来解构proc Int 。 我们将通过使用GADTs完成一个示例来证明这一点，以了解它正在做什么。 我们也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')
这为myExpr输出一个抽象语法树。 我们可以看到，如果expr的实现想要解构ProcSYM proc => proc Int值，它可以（并且在这种情况下）提供一个ProcSYM字典，它建立了知道如何解构的值。 我们可以在IntProc构造函数中看到这个值。
Expr (IntProc "proc A.")