Hacker News new | comments | show | ask | jobs | submit login
Mutable Algorithms in Immutable Languages, Part 3 (tel.github.io)
56 points by tel on July 15, 2014 | hide | past | web | favorite | 10 comments

Half baked thought.. more looking for discussion. :)

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

My understanding is that rust uses linear types. This could be done in a an embedded language in Haskell (even through just using Haskell's type system, albeit in a strange way).

Someone actually familiar with Rust should comment on what the typing systems used there actually involve, however.

"(even through just using Haskell's type system, albeit in a strange way)."

Tell me more! :)

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

I'm definitely going to need to come back to this a couple ties.


I highly recommend taking the time to read Oleg's entire Finally Tagless series. It is not easy material, but the technique is tremendous and his examples to explore it are packed with learning moments.

I shall!

I thought they got rid of the linear typing.

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

you might find this interesting: http://okmij.org/ftp/Haskell/regions.html

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact