你将如何抽象出这对"类似形状"数据类型中的样板

Question

一般问题

我有一对数据类型,它们是表示同一事物的两种不同方式,一种是在String中记录变量名,另一种是在Int中记录变量名.目前,它们都是定义的.但是,我想描述第一个表示,第二个表示将由某种关系生成.

具体例子

具体来说,第一个是STLC术语Universe的用户定义版本,而第二个是同一事物的de Bruijn索引版本:

{-# LANGUAGE RankNTypes, GADTs, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeFamilies, UndecidableInstances, FunctionalDependencies, FlexibleInstances  #-} 


-- * Universe of Terms * -- 

data Term :: Type -> * where 
    Var :: Id -> Term a
    Lam :: Id -> Type -> Term b -> Term (a :-> b)
    App :: Term (a :-> b) -> Term a -> Term b 

    Let :: Id -> Term a -> Term b -> Term b 
    Tup :: Term a -> Term b -> Term (a :*: b)
    Lft :: Term a -> Term (a :+: b)
    Rgt :: Term b -> Term (a :+: b)

    Tru :: Term Boolean
    Fls :: Term Boolean
    Uni :: Term Unit

data TermIn :: Type -> * where 
    VarI :: Idx -> Info -> TermIn a 
    LamI :: Type -> TermIn b -> Info -> TermIn (a :-> b)
    AppI :: TermIn (a :-> b) -> TermIn a -> TermIn b

    LetI :: TermIn a -> TermIn b -> Info -> TermIn b   
    TupI :: TermIn a -> TermIn b -> TermIn (a :*: b)

    TruI :: TermIn Boolean
    FlsI :: TermIn Boolean
    UniI :: TermIn Unit

-- * Universe of Types * --

data Type 
    = Type :-> Type
    | Type :*: Type
    | Type :+: Type
    | Boolean
    | Unit
    | Void

-- * Synonyms * --

type Id   = String          -- * variable name
type Idx  = Int             -- * de-brujin's index
data Info = Rec Id String   -- * store original name and extra info

已经有定义了一个关系Term和TermIn:

    class DeBruijnPair a b | a -> b, b -> a where 
        decode  :: b -> a
        encode  :: a -> b

    instance DeBruijnPair (Term a) (TermIn a) where
        decode = undefined
        encode = undefined 

请注意,因为原来的名字Term被储存在TermIn,有一个一到一个映射Term到TermIn,和背部.

重述问题

现在你可以看到涉及多少锅炉板,我想摆脱使用一些优雅的抽象,我定义Term和一些功能的类型输出TermIn.为了提供更多的背景,我正在为不同的lambda-calculus公式创建许多这样的外部和de Bruijn表示,并且一对一的关系适用于所有这些.

Answer 1

第一步骤是分离出特定于每个表示(零件Var,Lam,Let从定义的其余部分).

data AbstractTerm ? Type ? ? where
    App ? AbstractTerm (a :-> b) ? AbstractTerm a ? AbstractTerm b

    Tup ? AbstractTerm a ? AbstractTerm b ? AbstractTerm (a :*: b)

    Lft ? AbstractTerm a ? AbstractTerm (a :+: b)
    Rgt ? AbstractTerm b ? AbstractTerm (a :+: b)

    Tru, Fls ? AbstractTerm Boolean

    Uni ? AbstractTerm Unit

data Term ? Type ? ? where 
    Var ? Id ? Term a
    Lam ? Id ? Type ? Term b ? Term (a :-> b) 
    Let ? Id ? Term a ? Term b ? Term b 

data TermIn ? Type ? ? where 
    VarI ? Idx ? Info ? TermIn a 
    LamI ? Type ? TermIn b ? Info ? TermIn (a :-> b)
    LetI ? TermIn a ? TermIn b ? Info ? TermIn b   

然后,您需要将"通用"部分与您想要的具体表示相结合.将归纳定义构建为较小的块有一个众所周知的技巧:从数据类型中重构归纳调用,使子元素的类型成为类型的参数(在这种情况下,是类型的函数,因为你需要跟踪对象语言类型).

data AbstractTerm (t ? Type ? ?) ? Type ? ? where
    App ? t (a :-> b) ? t a ? AbstractTerm t b

    Tup ? t a ? t b ? AbstractTerm t (a :*: b)

    Lft ? t a ? AbstractTerm t (a :+: b)
    Rgt ? t b ? AbstractTerm t (a :+: b)

    Tru, Fls ? AbstractTerm t Boolean

    Uni ? AbstractTerm t Unit

data Term (t ? Type ? ?) ? Type ? ? where 
    Var ? Id ? Term t a
    Lam ? Id ? Type ? t b ? Term t (a :-> b)
    Let ? Id ? t a ? t b ? Term t b 

data TermIn (t ? Type ? ?) ? Type ? ? where 
    VarI ? Idx ? Info ? TermIn t a 
    LamI ? Type ? t b ? Info ? TermIn t (a :-> b)
    LetI ? t a ? t b ? Info ? TermIn t b   

要实例化此类型,可以使用归纳类型定义,该定义将自身与抽象类型相加以获取要赋予抽象类型的参数.

newtype ConcreteTermNamed ty
  = ConcreteTermNamed (Either (Term ConcreteTermNamed ty)
                              (AbstractTerm ConcreteTermNamed ty))

newtype ConcreteTermNameless ty
  = ConcreteTermNameless (Either (TermIn ConcreteTermNameless ty)
                                 (AbstractTerm ConcreteTermNameless ty))

这会引入一些额外的噪声,以选择是否需要在每个级别使用表示不可知或特定的术语,以及Haskell强制的新类型包装器,否则会保留您的术语语言.

var ? ConcreteTermNamed (Boolean :*: Unit)
var = ConcreteTermNamed
        (Right (Tup (ConcreteTermNamed (Left (Var "x")))
                    (ConcreteTermNamed (Left (Var "y")))))

fun ? ConcreteTermNamed (Boolean :-> (Unit :*: Boolean))
fun = ConcreteTermNamed (Left
        (Lam "b" Boolean
           (ConcreteTermNamed (Right
              (Tup (ConcreteTermNamed (Right Uni))
                   (ConcreteTermNamed (Left (Var "b"))))))))

这个技巧可用于对任意数量的不同归纳类型求和,通常用于将更大的语言分解为更小,更模块化的子语言; 例如,将AbstractTerm进一步分解为应用程序,产品,总和和单元类型,然后通过将它们添加到sum类型中将它们合并在一起可能是一种很好的方式.