Is there a way to use higher order abstract syntax with linear types?

Question

Is there a way to use HOAS style with linear types?

I'm also interested in affine types or other substructural systems.

I vaguely recall there has been some work for embedded DSLs for Haskell but I'm not sure if it would work just as fine for theorem proving.

I have a hunch you could do something like

Record Iso A B := {
  to: A -> B ;
  from: B -> A ;
  to_from x: to (from x) = x ;
  from_to x: from (to x) = x ;
}.
Class Linear (T: Set) := {
  lam: Iso T T -> T ;
  app: T -> T -> T ;
}.

But it seems a bit awkward to use in practice. I think that's probably the major problem with this kind of approach. Any encoding is going to be pretty heavy weight and not necessarily better than just using a typing context.

Answer 1

Yes. The basic idea is to give a HOAS encoding, and then define an auxiliary judgement which checks that variables are used linearly inside a term. Then your typing judgement has additional premises which check whether the term is being used linearly.

The Twelf wiki shows how to do it here.