3 ms·

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

by 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.

by tel 12y ago

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.