tel

73 ms·

661.
by tel 11y ago
I've got no problem with model checkers, though I'm not sure I agree with your effort ratings. Different tools for different jobs, eh? I think I also have a different conception of proof than you're naming. You don't nee
662.
by tel 11y ago
Yeah, I agree that it should be routinely called the C-H correspondence.
663.
by tel 11y ago
It's hard to say exactly. It will teach you to think of programming in an entirely new way. Will that make it easier to write good code elsewhere? Almost certainly if you're not familiar with mathematical proof (maybe you took a d
664.
by tel 11y ago
100% certainty in proof doesn't mean that you're aiming to get a 100% proven system. It means that you can stop worrying about the proven part forevermore. So it reduces long term running overhead.
665.
by tel 11y ago
As is traditional: You pronounce it with an understanding of how difficult it must be to speak French and have most of the CS world talk about bit twiddling.
666.
by tel 11y ago
Does Elm have a lens library?
667.
by tel 11y ago
In Elm you use static types to think of Javascript objects as static, anonymous records instead of dynamic dictionaries. There's a different type for that second use case with no syntax (just `get`). Theoretically this could enable a l
668.
by tel 11y ago
When you call a function f(x) it may, broadly, be the case that either the compiler knows exactly which function f is at compile time or f may be determined using information such as which x is being passed in—something only known during ru
669.
by tel 11y ago
Guo Juan's classes are fairly nice
670.
by tel 11y ago
It causes trouble for non-constructive logics, too. Any logic with an identity principle will be made inconsistent with the inclusion of `fix : forall a . (a -> a) -> a`. By yours are you referring to `forall a . a -> a`? I don&#x2
671.
by tel 11y ago
Fair enough.
672.
by tel 11y ago
Oh, I'm aware. It's just hard to always justify it and especially hard to do so in historical context.
673.
by tel 11y ago
Computation is something different. Models like call by push value make this very clear. LC does as well, though, but LC tends to be joined up with an equality semantics which intentionally sweeps computation under the rug for simplicity. T
674.
by tel 11y ago
In grad school I asked that so many times trying to figure out why it was the "right" solution and this historical cheat caused so much cognitive dissonance. Then again, on the other hand, "calculus works nicely" and &qu
675.
by tel 11y ago
It's not the type (a -> a) which is troubling, it's the type (forall a . (a -> a) -> a) which requires infinite looping. It's troubling precisely because the first type isn't.
676.
by tel 11y ago
I don't think at all that "value semantics" without any mention of complexity is an end in and of itself. Any sensible programmer will either (a) intentionally decide that performance is minimally important at the moment (and
677.
by tel 11y ago
I don't want to deny that those "quantitative" measures exist. I want to cast doubt that they're the dominant mechanism for modeling how real people think when they're accomplishing a task in a formal system.
678.
by tel 11y ago
For some reason I remember there being a web version of flow that was being compiled through js_of_ocaml. Maybe I'm confusing this with another project, though.
679.
by tel 11y ago
Non-termination, my bad! And of course that's true! Trivially so, though, in that we could do the same by picking the counter to be 10 instead of 2^1000, since we don't appear to care about changing the meaning of the program. If
680.
by tel 11y ago
So I sort of agree with you here, but only as a partial converse: > If all the formal semantic models for a language are unwieldy then you've probably got a non-simple language. Now, "simplicity" is a mental construct, a l
681.
by tel 11y ago
Purity can be defined very nicely against the arrows in a compositional semantics of a language and then effects follow as reasons for impurity. This is absolutely just a choice. It all ends up depending upon how you define equality of arro
682.
by tel 11y ago
Well, increasingly that's untrue as machine operation begins to become more data flow oriented. Even before it hits the machine optimizations are often better performed on analyses which are more "functional" in nature. SSA i
683.
by tel 11y ago
My understanding, though I've never personally made it explicit, is that you view "contra/covariance" as arising not as a property of vector spaces exactly (concretely) but instead from tensors-as-multilinear-maps and yo
684.
by tel 11y ago
As others have said, you can recover the notation exactly through category theory
685.
by tel 11y ago
They produce and use state when they run (at least in the Fold transformer format), but that's a very different kind of statefulness than generators.
686.
by tel 11y ago
Yeah, but they compose differently and are stateful. Transducers compose much like functions and are stateless.
687.
by tel 11y ago
It's not really map+reduce. Transducers arise out of realizing that transformations between (possibly infinite) lists can be encoded as a "reducer transformations", "transducers". When you work in this encoding you
688.
by tel 11y ago
It's worth noting as well that the flambda branch of the OCaml compiler is starting to include lots of these advanced optimizations which will (a) probably improve performance, (b) make abstraction more "free" enabling more u
689.
by tel 11y ago
It's trivial to via the use of types... So long as you have some amount of "purity" anyway.
690.
by tel 11y ago
The Haskell flavored tend to be clever ways to get a functional language without recursion.

More ›