2 ms·
> you occasionally stumble upon an abstraction leak, and then you need to take a really deep breath, climb down the abstraction ladder Can you give an example?
by tome 10y ago
> you occasionally stumble upon an abstraction leak, and then you need to take a really deep breath, climb down the abstraction ladder
Can you give an example?
- catnaroek 10y agoFor 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.