Try add pure and impure annotations

[mjgpy3]

@Kazark had a cool idea about restricting allowable programs such that

• impure code can call any code
• pure code can only call other pure code

I was thinking about it and, although it doesn't have an actual strong type system, it might be easy to extend mappy (probably in a fork) to try out this idea.

Since mappy is simple at the moment, I think the experiment could be achieved by

• parsing out a pure or impure annotation above each definition (failing if it's not given)
• Adding a compiler step to ensure the top restrictions
  • Currently the map __prim_io_map is the only way to do side-effecty things

@Kazark, what are your thoughts? Do we need a static type system to try this out?

[Kazark]

I was thinking of doing this in a statically typed language, but in an odd way it might almost be a more obvious fit for a dynamically typed language. After all, the point of it in a statically typed language is to be able to have the practicality of F# with a little extra cleanliness, i.e. to not have to use monads to write hello world. 😁 However, in a dynamically typed language, you aren't going to be able to enforce purity with monads.

Seems like you should be able to do it in a dynamically typed language I suppose, though in an odd way it's almost like a real thin layer of static type checking.

Another thing I've thought of is to allow opt-in totality in a similar way. Without dependent types there are a large number of things that you just plum wouldn't be able to make total, so it may not be very useful. However perhaps there would be certain times when you can and would want to enforce totality.

[mjgpy3]

in an odd way it might almost be a more obvious fit for a dynamically typed language [...] in a dynamically typed language, you aren't going to be able to enforce purity with monads

That's a great point

though in an odd way it's almost like a real thin layer of static type checking

Kind of, right? I mean, Haskell and family use IO to represent, well, IO but are side-effects necessarily a type?

Opt-in totality sounds interesting. How would it differ from Idris' totality "directives"?

[Kazark]

My idea with totality would be superficially the same, and perhaps in many ways at the core the same as totality in Idris. The main difference would be, totality is a lofty goal even with dependent types, and without them it really limits what you can do. But I would still be intrigued to try it.