I am directly suffering *something*, as I take parts of one rather large codebase (QEMU) and use their remote state to inform state changes in other components. I am attempting to compose, and I am experiencing friction. I get through it, of course, but it rhymes with your take.
-
-
Replying to @dakami @andreasdotorg
I am 100% OK if you are actually describing something else, that only rhymes to my remote ear.
0 replies 0 retweets 1 like -
Replying to @typeswitch @andreasdotorg
Types and definitions are different things? I thought you defined types.
2 replies 0 retweets 0 likes -
Replying to @dakami
We're in dependent type land here. Simplyfing things here, types are functions. It makes sense to think of them in terms of interface and implementation. Now here's the catch: "a+b" and "b+a" compute the same value, but they are different types, as they look different. Ouch.
1 reply 0 retweets 3 likes -
Replying to @andreasdotorg
Is commutation required for addition? a+b could return an object of type a, while b+a could return an object of type b, calling different thunking functions. That is a degree of freedom languages have.
1 reply 0 retweets 0 likes -
Replying to @dakami
Are you thinking in types here? I'm not talking about the type *of* "a+b", I'm talking about the *type* "a+b". When both a and b are Nat, a+b clearly is of type Nat. So is b+a.
1 reply 0 retweets 1 like -
Replying to @andreasdotorg
Like I said, I come from practical considerations that validate theoretical constructions. a+b has an output of some type. That type can, I suppose, be lazily computed as the output of a+b. Which is still not the output of b+a. Lazy resolution eventually hits a wall.
2 replies 0 retweets 0 likes -
Replying to @dakami
We're talking about the same function + here in both cases. Also, a and b have the same type, which happens to be the type that + returns. Nothing magic here, really. The fundamental issue is that I have to invoke cummutativity explicitly. It leaks abstractions.
2 replies 0 retweets 0 likes
I just happen to have that example in all its painful depth... http://docs.idris-lang.org/en/latest/proofs/index.html … FWIW I agree we need to do much better here.
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.