3 ms·
For most type classes and instances, the proofs that the corresponding laws hold break horribly if you substitute their free variables with nonterminating compu
by catnaroek 10y ago
For most type classes and instances, the proofs that the corresponding laws hold break horribly if you substitute their free variables with nonterminating computations. For instance, `0 * x = 0` doesn't hold if `x` is `undefined`.
- sclv 10y agoYou do get 0 * x <= 0. You just need a splash of domain theory to make the medicine go down.
- tome 10y agoI don't think that's the <= you were looking for ...
- tome 10y agoHow would a strict language help? `0 * x = 0` doesn't hold if `x` is substituted by a non-terminating computation `f ()`. What exactly would be the benefit?
- catnaroek 10y agoIn a strict language, non-terminating computations aren't values in the first place. So you can't substitute `x` with bottom.
- tome 10y agoI don't think I've grasped the distinction between substituting a variable of type t with a value of type t versus an expression of type t.
- catnaroek 10y agoThere's no such distinction. But, in the operational semantics of a call-by-value language, variables are only substituted with values. Or, to be consistent with the terminology I've used in other comments, in any language, a value is something a variable can be substituted with. It's just that, in a call-by-value language, variables can never be substituted with unfinished computations.