Mutable Algorithms in Immutable Languages, Part 3

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

They may have, I'm not following it closely.