ebingdom

6 ms·

1.
by ebingdom 4y ago
Yeah, I only meant as opposed to judgmental equality, not the quality of being a proposition.
2.
by ebingdom 4y ago
> It was to provide a small, parsimonious foundation for all of mathematics with a minimal number of "obvious" commitments, to give us confidence that the mathematics we're doing is consistent I would argue that type theor
3.
by ebingdom 4y ago
> I do not understand why homotopy type theory posts are so popular on this website. Martin-Löf type theory (and, therefore, homotopy type theory) is like an idealized programming language that is capable of expressing both programs and
4.
by ebingdom 4y ago
For people who know Rust, Haskell's type classes are like a more general version of Rust's traits. But that comparison suggests the wrong chronology; Haskell's type classes came a couple decades earlier.
5.
by ebingdom 4y ago
It's not about biases. Using immutability is not just some personal preference. It's common knowledge that mutability everywhere is a bad practice. That's why there's a trend toward immutability by default in newer langu
6.
by ebingdom 4y ago
> Thankfully, this sort of analysis tends to use "constructive logic"; in which case, we're told why some property isn't provable (either because we're given a counterexample proving it's incorrect, or we&#x
7.
by ebingdom 4y ago
That's a ridiculously high bar to set before you recognize any progress being made.
8.
by ebingdom 4y ago
> The net effect of this would be that I type "mutable" all over the place You might want to consider adopting a more modern programming style for the benefit of your coworkers (and possibly yourself). Mutability all over the p
9.
by ebingdom 4y ago
> Reasoning About Software What's wrong with this? I need a way to describe techniques that make it easier to...well I don't even know another way to say it. Maybe I'm biased by my experience in formal verification, a fiel
10.
by ebingdom 4y ago
I think there might be a loose connection. When you want to prove something using mathematical induction, you must come up with an "induction hypothesis". This requires cleverness which could possibly be described as the product o
11.
by ebingdom 4y ago
> It's a bit strange that it got BigInt before Int64 JavaScript has Int64?
12.
by ebingdom 4y ago
> I wish that all language design went through a filter where every character mattered like the designer was in an episode of Squid Game. Yes, I totally support this! Coming from languages like Haskell, most languages look so unnecessari
13.
by ebingdom 4y ago
As someone with years of experience writing machine-checked proofs in Coq, I cannot imagine the term "Software Engineer" shifting to that meaning, even though it may make sense when compared to other engineering disciplines. The p
14.
by ebingdom 4y ago
> You might say "but it will make it more confusing for people who already know the FP terms" People who already know FP would be fine. Newcomers would be the ones to suffer. We already have a large number of tutorials, blogs,
15.
by ebingdom 4y ago
This is a really uninformed opinion. I'm disappointed that it's currently the top comment. You really think functional programmers don't build composite types?
16.
by ebingdom 4y ago
I agree about the math terminology, but I think it would be more confusing if we created a completely different set of vocabulary for the same concepts. So I don't really know what to do: refer to something by its proper name, or creat
17.
by ebingdom 4y ago
> The lambda calculus is an entirely arbitrary way to organize things in math. It’s not based on nature or truth at all. Lambda calculus, category theory, and logic are essentially 3 sides of the same coin (the Curry-Howard-Lambek corres
18.
by ebingdom 4y ago
I wonder why they don't just use the highest precision possible given whatever representation of numbers they're using? I know these extra digits would be unlikely to ever matter in practice, but why even bother truncating more th
19.
by ebingdom 4y ago
Categories are objects and morphisms with identities and composition, subject to some coherence laws characterizing identities and stating the associativity of composition. Category theory studies categories and related constructions, such
20.
by ebingdom 4y ago
This article is completely incongruous and reveals fundamental misunderstandings of category theory. That's actually being generous; most of the content isn't even coherent enough to be wrong. > Category Theory (at least applie
21.
by ebingdom 4y ago
> but does that mean it's a good idea? Yes, to me it does. I love when variables have really tight scopes so I don't need to worry about if/how they are used throughout the rest of the program. Locality should be the defau
22.
by ebingdom 4y ago
> Cold start (time to first response, ms) O(100) O(1000) O(10000) Ugh, that's not how big O notation works.
23.
by ebingdom 4y ago
> Welcome to Move, a next generation language for secure, sandboxed, and formally verified programming. I didn't see anything about formal verification in the rest of the documentation. Does it have dependent types? Does it have a m
24.
by ebingdom 4y ago
Until wasm provides a way to release memory pages, nah.
25.
by ebingdom 4y ago
That's an interesting idea, but how does it work for functions of multiple arguments? If functions are curried, then I suppose the syntax for `f x y` would be `y.(x.f)`, which maybe you could write as `y.x.f` if the associativity worke
26.
by ebingdom 4y ago
> static typing is less expressive than dynamic typing Here's something I can express with static typing that I can't express with dynamic typing: "this function returns a function which returns an integer for every input&
27.
by ebingdom 4y ago
> Discipline doesn't scale. I want a shirt with this on it.
28.
by ebingdom 4y ago
As a Haskell programmer, this argument does not resonate with me. I find most dynamically typed languages (e.g., JavaScript) verbose compared to what I'm used to. Of course, plenty of statically typed languages are verbose too. But sta
29.
by ebingdom 4y ago
Those languages don't have null safety, but plenty of languages do. Rust, Kotlin, Swift, Haskell, etc. The claim is true: a type system _can_ prevent null-related issues and eliminate the need to account for them in tests. That's
30.
by ebingdom 4y ago
Also the Rust compiler was originally written in OCaml. Not that that necessarily implies a parent-child relationship between the languages, but it's clear OCaml was on the minds of the original Rust developers.

More ›