tel

101 ms·

931.
by tel 11y ago
Well, you can run multiple simultaneous particle chains and sum their results. There's some wasted work since each will need to burn in, but modern algorithms can make that go quite quickly.
932.
by tel 11y ago
That wasn't really in the core verifier exactly. It was more like an optimization.
933.
by tel 11y ago
Sure. I'm not super familiar with F#, but I can state things which depend upon functors. A good example is the Set.Make functor in the OCaml stdlib. Elements in a Set must be orderable for efficiency's sake, so to construct a Set
934.
by tel 11y ago
Type classes are far less direct to encode. One also requires existential types to get the modularity properties of ML modules and they are a burden to deal with in Haskell. A good example of something easy to do with ML modules and hard to
935.
by tel 11y ago
Functors tend to be the big thing that's missing, right? F# just had to drop the feature because of compatibility with .Net packages, as I understand, but it severely cripples the module system. MLs are such that the value-level stuff
936.
by tel 11y ago
Well, sure, but it's probabilistic and delayed punishment. This makes learning habits and ensuring them difficult.
937.
by tel 11y ago
The problem is that without a linter there's no punishment for missing semicolons. So really the argument should be that everyone should use a linter.
938.
by tel 11y ago
variance is used in Haskell all the time . Haskell's subtyping/type-subsumption relation is less pervasive than an OO language's, but it's critical. Furthermore, variance is more fundamental than subtyping. It is not
939.
by tel 11y ago
Sounds really interesting! I look forward to seeing more
940.
by tel 11y ago
Agreed. (Syntactic) types are exactly incoherent with the kind of "spooky action at a distance" that mutability enables. Semantic type layers could do more, perhaps.
941.
by tel 11y ago
Covariance and contravariance are intimately related to "mapping" and only incidentally related to subtype polymorphism. In particular, if we assume we have a function coerce : a -> b which can only be applied when a i
942.
by tel 11y ago
Sometimes your problem really does just call for a hammer :)
943.
by tel 11y ago
Yeah, depends on how you're encoding it. Quotient types are to my knowledge still tricky to implement, but you can try to make a setoid and structure this type with some kind of equality. Of course, now we run directly into totality an
944.
by tel 11y ago
Streams are coinductive, thus reals are the type of final coalgebras of (rat * -) which satisfy the Cauchy condition. So something like (Sigma (mu (rat * -)) isCauchy).
945.
by tel 11y ago
There's a topological direction... but I have to agree that calculus is much more conceptually immediate to humans anyway. But even a disembodied being of pure reason might eventually discover continuity via logic->topology.
946.
by tel 11y ago
You also need to translate "with" as a forall (pi binder) as well. Then, you'll merely note that the formula is unsatisfiable without demonstrating a proof that y is within the proper bounds.
947.
by tel 11y ago
I've seen an impl somewhere where the (int => rat) bit from the Isabelle/HOL design was (stream rat). That's about the best I have at the moment.
948.
by tel 11y ago
I haven't read the paper, but if you define the reals as constructive Cauchy sequences you'd be forced into a coinnductive definition. Is that equivalent?
949.
by tel 11y ago
to_nil is actually a pretty important function! Completely trivial, obviously, but it demonstrates that there's a canonical way to map every value in Ruby to nil. This is essentially the defining feature of nil, in a sense. With typing
950.
by tel 11y ago
Modules can be seen as a collection of types (abstract or otherwise) and functions acting upon those types. Very prosaically, this can just be a type parameterized dictionary (or vtable if that floats your boat). Haskell's "constr
951.
by tel 11y ago
Well, it certainly spent effort explaining JS oddities, but it's ostensibly about OCaml modules. So, it's either stream of consciousness and dependent on commentary to intuit meaning or merely failed in its goal.
952.
by tel 11y ago
This is pretty wacky. I cannot help but feel that it would be far better to just learn OCaml modules without this metaphor. It seems too far from meaningful.
953.
by tel 11y ago
Huh, yeah. I don't really enjoy semantic arguments, either, but I think you've got a lot of great points. There is something really genuinely different about a "DSL" which has reached the status of being totally external
954.
by tel 11y ago
Mostly we're just expressing a difference of opinion, but one thing that I'd like to contest is that the goal of the Zen of Python is to produce developer happiness. In particular, I'll state that my cherry picking from that
955.
by tel 11y ago
So, in your mind compilation is what distinguishes a DSL from... something else?
956.
by tel 11y ago
I strongly approve of this message. I think the reason why Ruby has such terrible DSLs is not due to its technological strengths or weaknesses but instead because the community promotes the idea that a good DSL is super human readable. I&#x
957.
by tel 11y ago
Before you start throwing insults, what exactly is a language to you? I'm pretty confident that determining the difference between a language and an API is not so easy a thing to do.
958.
by tel 11y ago
Sorry, I'm just writing in Typescript. It's the typed Javascript flavor I'm most familiar with. But, yep, you properly erased the types. I'd love to use Haskell-to-JS but I don't think I could bet a product on it qu
959.
by tel 11y ago
Sure, you can represent it that way, but it needlessly complicates the semantics of `then`. If they were merely monadic bind then it'd easily be 1/20th as confusing. The "overload everything every which way and assume that
960.
by tel 11y ago
So alpha convert your names to whatever you like. I don't know how to do it namelessly in Javascript without Chuch encoding the pair. You can go much further than this. The following operation ap<A, B>(pf: Promise<(a: A)

More ›