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.


1 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.

  • $\begingroup$ Thank you . For some reason your link is broken but I was able to search up the page anyway. I played a bit with this sort of approach but it's a bit clumsy in Coq. gist.github.com/mstewartgallus/052eabf8044e23ecfb678bf92931d9d8 $\endgroup$ Commented May 20, 2022 at 22:32
  • $\begingroup$ I'd guess the problem with the link is that twelf.org does not support https: (only http:). $\endgroup$
    – hardmath
    Commented May 22, 2022 at 13:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.