systematize typesafe conversions for terms

[wisnesky]

The up, up14, up15, etc functions convert from Term ... Void ... to Term ... X ... . This issue is to systematize these, i.e.,

upGen :: Term (Gen=Void) ... -> Term (Gen=X) upSk :: Term (Sk=Void) ... -> Term (Sk=X) UpGenSk :: both

etc

[wisnesky]

whoever does this definitely needs to take a giant lock first

[wisnesky]

Term is 8-functor, maybe this could help: https://hackage.haskell.org/package/n-ary-functor-0.1.0.0/docs/NAryFunctor.html

[wisnesky]

If this works then Term can possibly turn into a GADT:

data Term :: * * * * * * * * -> * where
  = Var var :: Term var Void Void Void Void Void Void Void

  | Sym sym  [Term var ty sym en fk att gen sk] :: Term var ty sym en fk att gen sk

  | Fk  fk   (Term var Void Void en fk Void gen Void) :: Term var Void Void en fk Void gen Void

  | Att att (Term var Void Void en fk Void gen Void) :: Term var Void Void en fk att gen Void

  | Gen gen :: Term Void Void Void Void Void Void gen sk

  | Sk  sk :: Term Void Void Void Void Void Void Void sk

[wisnesky]

It's possible to turn the Exps into GADTs as well, but doing so might be counterproductive. I think you really need sigma types instead of existentials to see a win but it would be an interesting experiment.

[wisnesky]

What do you guys think about something like this:

class Convertible a b where
 convert :: a -> b

instance Convertible Void a where
 convert = absurd

polymorphicConvert 
 :: (Convertible var var', Covertible ty ty', ...) => Term var ty ... -> Term var' ty'
polymorphicConvert (Var v) = Var $ convert v
,,,