Как бы вы абстрагироваться от шаблонного в этой паре «похожи фасонных» типов данных

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 

Затем вам необходимо объединить «общую» часть с конкретным изображением, которое вы хотите. Известный трюк для создания индуктивных определений на более мелкие куски: вы реорганизуете индуктивный вызов из типа данных, делая типы подэлементов параметром для типа (в данном случае функцию над типом типа, так как вам нужно отслеживать тип объекта-типа).

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 мандат Newtype обертка, но в противном случае оставляет свой термин языка, как это было.

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 дальше на типы приложений, продуктов, сумм и единиц, а затем объединить их все вместе, добавив их в тип суммы.