6

一般问题

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

具体例子

具体来说，第一个是 STLC 术语全域的用户定义版本，而第二个是同一事物的 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

已经在Termand上定义了一个关系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之间存在一对一的映射。TermTermIn

重述问题

现在您可以看到涉及多少样板，我想使用我定义的一些优雅的抽象Term和类型输出的一些函数来摆脱它TermIn。只是为了提供更多上下文，我正在为不同的 lambda 演算公式创建许多这样的外部和 de Bruijn 表示对，并且一对一的关系适用于所有这些。

4

1 回答 1

6

第一步是将特定于每个表示的部分（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

然后，您需要将“通用”部分与您想要的具体表示相结合。将归纳定义构建成更小的块有一个众所周知的技巧：你重构数据类型的归纳调用，使子元素的类型成为类型的参数（在这种情况下，你的 Type 类型的函数，因为您需要跟踪对象语言类型）。

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 进一步拆分为 application、product、sum 和 unit 类型，然后通过将它们添加到 sum 类型中将它们合并在一起可能是一种很好的风格。

于 2014-01-28T05:10:17.500 回答