You can encode it in Finally Tagless Style [0] basically as an extension of the strongly typed de Bruijn indexed lambda calculus. Here's de Bruijn class De

You can encode it in Finally Tagless Style [0] basically as an extension of the strongly typed de Bruijn indexed lambda calculus. Here's de Bruijn class DeBruijn r where z :: r (a, h) a s :: r h a -> r (any, h) a lam :: r (a, h) b -> r h (a -> b) app :: r h (a -> b) -> r h a -> r h b which might be a little easier to read in HOAS form (it's certainly prettier) class HOAS r where lam :: (r a -> r b) -> r (a -> b) app :: r (a -> b) -> (r a -> r b) Anyway, if you extend the idea of the tupled free variable environment denoted by the second parameter to `r` in the `DeBruijn` class above to have "unused" and "used" variables then you can enforce linearity. To do this we encode a "type-level maybe" demonstrating we may or may not actually have a type variable to use newtype F a = F a data U = Used class LDeBruijn r where z :: r (F a, h) (U, h) a s :: r hi ho a -> r (any, hi) (any, ho) a app :: r hi h (a -> b) -> r h ho a -> r hi ho b lam :: r (F a,hi) (U,ho) b -> r hi ho (a -> b) Kind of. Really it's a bit more complex since in order to actually execute statements of these types you need to do a bit more work. Creating evaluators for `DeBruijn` or `HOAS` is quite easy, but you need to do some type-level work for `LDeBruijn`. See the article itself for more. [0] http://okmij.org/ftp/tagless-final/course/#linear http://okmij.org/ftp/tagless-final/course/#linear