4 ms·

Since when does static typing imply monads...

choeger 6y ago
Actually, it does. If you want a sound and complete static type system for a practical language, you end up with monads (or something very close to it, like streams or effects) or you cannot type your side effects (and then your type system is either incomplete or your language impractical).
- skrebbel 6y ago
  You don't need a sound type system for the language to be practical though. Eg C#, Kotlin, TypeScript.
- tomcam 6y ago
  Argh this sounds interesting but I’m not smart enough to make the connections. Could you dumb the explanation down a bit?
  - lostcolony 6y ago
    It's just saying that your type system is incomplete if it doesn't capture side effects. That is, if the function can do something that is not expressed as part of its return type, its return type is insufficiently expressive. As an example, imagine an "updateDB" call that returns void. Totally could exist, and be useful, but all it does is a side effect; as a function you haven't expressed its functionality via its type. From a 'pure' perspective, it would be fair for the compiler to remove that call entirely, since you do nothing with the result (since there is no result). Instead you need a monad or something to express that side effect. Obviously, many languages don't choose to express side effects within their type systems. It's not that means the language isn't useful, just that its type system isn't complete; you have things happening without a type attached to them (and in that way it's dynamically typed).
    - tomp 6y ago
      Monads don't help you there, though. Even Haskell doesn't capture the effect of "division by zero". In the end, type systems (all of them, static as well as dynamic) are just a tradeoff between safety and practicality.
    - choeger 6y ago
      The problem is more that you cannot formally express your type system in such a case. The "pure" perspective you mentioned is basically the limited view that one can still work with when defining a type system. Side effects are then basically magic functions that have any necessary type (in fact, OCaml has such a function in its stdlib, called "magic", if I am not mistaken).
- Hercuros 6y ago
  What does it mean for a type system to be “complete”? Type soundness means that well-typed programs do not “get stuck”, but it is not obvious at all (at least to me) what it means for a type system to be complete, formally speaking. If you just mean that a program has certain properties (like performing IO) that are not expressed in its type, then I can see what you mean. But even in Haskell, some properties like “this function might fail to terminate or throw an exception” are not expressed in the type (although you can use monads for those things in languages where all functions terminate by default). There are no distinctions between a function that performs network accesses and one that does not, or functions that never return odd numbers, etc. There are infinitely many program properties that you can come up with which are not expressible in Haskell types. Even dependently typed languages with very expressive type systems cannot capture all possible program properties due to logical incompleteness results.
  - choeger 6y ago
    A type system is complete when every error-free program is well-typed. This is, afaik, seldom the case. I was using the term more informally. In fact it is the operational semantics of your hypothetical language that is not complete in the sense that you will have a hard time putting it into a form that allows you to do anything meaningful (e.g. proof absence of certain errors) with it. Interestingly, you can define such a language with side effects (think ML), by actually pulling the state monad into your meta-level (for instance by turning your reduction relation into an instance of a state monad).
- HelloNurse 6y ago
  Practically, what ways to "type your side effects" are useful and not only mandatory formalities to appease the compiler? For example, writing something or something else or nothing at all to the standard output doesn't appear likely to influence the execution of the rest of the program, even if formally the program is in a different state.
skrebbel 6y ago
Static typing and a useful option type in an ecosystem without null pretty much implies monads I think (or lots of boilerplate)

Actually, it does. If you want a sound and complete static type system for a practical language, you end up with monads (or something very close to it, like streams or effects) or you cannot type your side effects (and then your type system is either incomplete or your language impractical).

skrebbel 6y ago
You don't need a sound type system for the language to be practical though. Eg C#, Kotlin, TypeScript.
tomcam 6y ago
Argh this sounds interesting but I’m not smart enough to make the connections. Could you dumb the explanation down a bit?
- lostcolony 6y ago
  It's just saying that your type system is incomplete if it doesn't capture side effects. That is, if the function can do something that is not expressed as part of its return type, its return type is insufficiently expressive. As an example, imagine an "updateDB" call that returns void. Totally could exist, and be useful, but all it does is a side effect; as a function you haven't expressed its functionality via its type. From a 'pure' perspective, it would be fair for the compiler to remove that call entirely, since you do nothing with the result (since there is no result). Instead you need a monad or something to express that side effect. Obviously, many languages don't choose to express side effects within their type systems. It's not that means the language isn't useful, just that its type system isn't complete; you have things happening without a type attached to them (and in that way it's dynamically typed).
  - tomp 6y ago
    Monads don't help you there, though. Even Haskell doesn't capture the effect of "division by zero". In the end, type systems (all of them, static as well as dynamic) are just a tradeoff between safety and practicality.
  - choeger 6y ago
    The problem is more that you cannot formally express your type system in such a case. The "pure" perspective you mentioned is basically the limited view that one can still work with when defining a type system. Side effects are then basically magic functions that have any necessary type (in fact, OCaml has such a function in its stdlib, called "magic", if I am not mistaken).
Hercuros 6y ago
What does it mean for a type system to be “complete”? Type soundness means that well-typed programs do not “get stuck”, but it is not obvious at all (at least to me) what it means for a type system to be complete, formally speaking. If you just mean that a program has certain properties (like performing IO) that are not expressed in its type, then I can see what you mean. But even in Haskell, some properties like “this function might fail to terminate or throw an exception” are not expressed in the type (although you can use monads for those things in languages where all functions terminate by default). There are no distinctions between a function that performs network accesses and one that does not, or functions that never return odd numbers, etc. There are infinitely many program properties that you can come up with which are not expressible in Haskell types. Even dependently typed languages with very expressive type systems cannot capture all possible program properties due to logical incompleteness results.
- choeger 6y ago
  A type system is complete when every error-free program is well-typed. This is, afaik, seldom the case. I was using the term more informally. In fact it is the operational semantics of your hypothetical language that is not complete in the sense that you will have a hard time putting it into a form that allows you to do anything meaningful (e.g. proof absence of certain errors) with it. Interestingly, you can define such a language with side effects (think ML), by actually pulling the state monad into your meta-level (for instance by turning your reduction relation into an instance of a state monad).
HelloNurse 6y ago
Practically, what ways to "type your side effects" are useful and not only mandatory formalities to appease the compiler? For example, writing something or something else or nothing at all to the standard output doesn't appear likely to influence the execution of the rest of the program, even if formally the program is in a different state.

skrebbel 6y ago

Static typing and a useful option type in an ecosystem without null pretty much implies monads I think (or lots of boilerplate)