I've checked out Rust a bit, and their approach to memory safety seems pretty novel, by statically tracking where a piece of memory is being used in computation and only allowing it to be used once at any point in time.
Seems like using Mem can bring back all those mutable errors in stateful languages, would it be possible to apply the Rust memory model to Mem?
Side note: #haskell on IRC is an awesome place to discuss PLT :D
Someone actually familiar with Rust should comment on what the typing systems used there actually involve, however.
Tell me more! :)
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
class HOAS r where
lam :: (r a -> r b) -> r (a -> b)
app :: r (a -> b) -> (r a -> r b)
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)