Quite a while back, I wrote:
On Thu, Jul 3, 2014 at 11:06 AM, Jonathan S. Shapiro <[email protected]>
wrote:
>
> And it *definitely* pushes us to multivariable type classes, because in
> (e.g.) "1 + 2" at the type level, + is a functor having type 'a x 'b -> 'c
>
I stumbled across it today, and I'm not sure why I thought this. It really
isn't at all clear to me why + as a functor requires type 'a x 'b -> 'c.
The context of the original question was dependent types. What occurs to me
now is that admitting dependent types does not inherently mean that things
like (+) need to cross strata.
And of course, now that I write that, it's perfectly obvious why we want +
to do that:
def AddNatOne x is
let NatOne = 1 :: nat
x + NatOne
OK. Good. Now I can go back to something productive. There are moments in
this process when I just want to slap myself on the forehead and say "doh".
:-)
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
