How would you abstract the template in this pair of "similar forms"

Question

General question

I have a couple of data types that are two different ways of representing the same thing: one writes the variable name to String, and the other writes the variable name to Int. They are both currently defined. However, I would like to describe only the first view, and the second in some way.

Specific example

Specifically, the first is the user version of the term STLC term, and the second is the de Bruijn version of the same thing:

{-# 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 index data Info = Rec Id String -- * store original name and extra info 

There is already a relationship defined over Term and TermIn :

  class DeBruijnPair ab | a -> b, b -> a where decode :: b -> a encode :: a -> b instance DeBruijnPair (Term a) (TermIn a) where decode = undefined encode = undefined 

Note that since the original TermIn name is stored in TermIn , there is a one-to-one mapping from Term to TermIn and vice versa.

Repeat question

Now you can see how many boiler plates are involved, which I would like to get rid of using an elegant abstraction, where I define Term and some functions on terminals of TermIn types. To provide an even larger context, I create many pairs of such external and de Bruyne representations for various formulas of lambda calculus, and for all of them there is a one-to-one relationship.

Answer 1

The first step is to separate the parts that are specific to each view ( Var , Lam , Let ) from the rest of the definitions.

 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 

Then you need to combine the “common part with the specific representation you want. There’s a well-known trick for creating inductive definitions into smaller pieces: you will reorganize the inductive call from the data type, making the sub-element types a parameter for the type (in this case, a function over the type of the type , since you need to track the type of object-object).

 data AbstractTerm (t ∷ Type → ★) ∷ Type → ★ where App ∷ t (a :-> b) → ta → AbstractTerm tb Tup ∷ ta → tb → AbstractTerm t (a :*: b) Lft ∷ ta → AbstractTerm t (a :+: b) Rgt ∷ tb → AbstractTerm t (a :+: b) Tru, Fls ∷ AbstractTerm t Boolean Uni ∷ AbstractTerm t Unit data Term (t ∷ Type → ★) ∷ Type → ★ where Var ∷ Id → Term ta Lam ∷ Id → Type → tb → Term t (a :-> b) Let ∷ Id → ta → tb → Term tb data TermIn (t ∷ Type → ★) ∷ Type → ★ where VarI ∷ Idx → Info → TermIn ta LamI ∷ Type → tb → Info → TermIn t (a :-> b) LetI ∷ ta → tb → Info → TermIn tb 

To create an instance of this type, you can use an inductive type definition that sums with an abstract type to get a parameter that gives an abstract type.

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

This adds a little extra buzz to choose whether you want to be an agnostic or -specific term at each level, as well as the newtype shell assigned by Haskell, but otherwise leaves your terminology as it is.

 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")))))))) 

This trick can be used to summarize any number of different inductive types and is often used to break up a larger language into smaller, more modular sublanguages; for example, it might be a good style to further divide your AbstractTerm into application types, products, amounts, and units, and then combine them all together by adding them to the amount type.