5 ms·

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 trackin

by munro 12y ago

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

tel 12y ago
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.
- dllthomas 12y ago
  "(even through just using Haskell's type system, albeit in a strange way)." Tell me more! :)
  - tel 12y ago
    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
    - dllthomas 12y ago
      I'm definitely going to need to come back to this a couple ties. Thanks!
      - tel 12y ago
        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.
        dllthomas 12y ago
        I shall!
- oconnor0 12y ago
  I thought they got rid of the linear typing.
  - tel 12y ago
    They may have, I'm not following it closely.
zem 12y ago
you might find this interesting: http://okmij.org/ftp/Haskell/regions.html http://okmij.org/ftp/Haskell/regions.html

by munro 12y ago

tel 12y ago

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.

dllthomas 12y ago
"(even through just using Haskell's type system, albeit in a strange way)." Tell me more! :)
- tel 12y ago
  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
  - dllthomas 12y ago
    I'm definitely going to need to come back to this a couple ties. Thanks!
    - tel 12y ago
      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.
      - dllthomas 12y ago
        I shall!
oconnor0 12y ago
I thought they got rid of the linear typing.
- tel 12y ago
  They may have, I'm not following it closely.

zem 12y ago

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