Как бы вы абстрагировали шаблон в этой паре "похожих по форме" типов данных?

Question

Общий вопрос

У меня есть пара типов данных, которые представляют собой два разных способа представления одной и той же вещи: один записывает имя переменной в String, а другой записывает имя переменной в Int. В настоящее время они оба определены. Тем не менее, я хотел бы описать только первое представление, а второе будет порождено некоторым отношением.

Конкретный пример

Конкретно, первая - это пользовательская версия юниверса термина STLC, а вторая - индексированная версия де Бруйна того же самого:

{-# 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, Просто чтобы предоставить еще больше контекста, я создаю много пар таких внешних представлений и представлений де Брейна для различных формулировок лямбда-исчисления, и отношение один-к-одному имеет место для всех них.

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   

Затем вам нужно объединить "общую" часть с конкретным представлением, которое вы хотите. Существует известная хитрость в построении индуктивных определений в более мелкие порции: вы реорганизуете индуктивный вызов из типа данных, делая типы подэлементов параметром для типа (в данном случае, функцией над вашим типом 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, но в остальном оставляет ваш термин language таким, каким он был.

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 далее на типы приложения, product, sum и unit, а затем объединить их все вместе, добавив их в тип sum.