News for hackers. Stuff that matters.

A comment on Why GitHub used Haskell for Semantic. Parent comment

Re:Why GitHub used Haskell for Semantic by quickthrower2 on Wednesday June 05, 2019 @10:42PM (#20111135)
Not used Clean, but it sounds interesting.

What i'd love is an imperative language where you declare what effects a method can have and the compiler enforces them. E.g. if it promises not to mutate any parameters, it can only call functions that make the same promise etc.

[ Parent | on HN ]
Re:Why GitHub used Haskell for Semantic by cinnamonheart on Thursday June 06, 2019 @09:42AM (#20114421)
Idris isn't imperative (Haskell-like with dependent types), but offers features like those:

http://docs.idris-lang.org/en/latest/effects/depeff.html

    readInt : Eff Bool [STATE (Vect n Int), STDIO]
                       [STATE (Vect (S n) Int), STDIO]
http://docs.idris-lang.org/en/latest/st/machines.html

    logout : (store : Var) -> ST m () [store ::: Store LoggedIn :-> Store LoggedOut]
They're both implemented within Idris, as libraries/modules, rather than being compiler magic:

- https://github.com/idris-lang/Idris-dev/blob/master/libs/con...

- https://github.com/idris-lang/Idris-dev/blob/master/libs/eff...

I think it'd be possible to write similar effect systems in other dependently typed languages like ATS, which is a relatively imperative language (C+ML-like).

[ Parent | on HN ]
Re:Why GitHub used Haskell for Semantic by malvosenior on Wednesday June 05, 2019 @11:38PM (#20111361)
That sounds very similar to Rust. Mutations and even memory lifetime are specified in the type system.
[ Parent | on HN ]
Re:Why GitHub used Haskell for Semantic by brabel on Thursday June 06, 2019 @06:45AM (#20113233)
This is how Pony does it, basically. See [Reference Capabilities](https://tutorial.ponylang.io/reference-capabilities.html).
[ Parent | on HN ]