creata

40 ms·

691.
by creata 5y ago
> This is probably just not how things work in Haskell and I just need to be okay with that. Yep, that's just how things work in Haskell: disjoint unions are much simpler regular unions, and they're usually what you want in the
692.
by creata 5y ago
You mean ∑ and Σ? Yeah, that'd be terrible. It doesn't seem like it should be Unicode's job to assign meaning to characters, so I don't know why ∑ ("U+2211 N-Ary Summation") exists.
693.
by creata 5y ago
For anyone on Vim, you can insert lots of special characters by hitting Ctrl+K: =3 is ≡, -> is →, l* is λ, M- is —, etc. You can also run :dig! to see a list of all digraphs, and :help digraph for information on how to define your own.
694.
by creata 5y ago
Alright, that's fine, but the person I replied to was complaining that "Haskell folks love arrows and one letter variable names", and my point was that most programmers love one letter variable names in this context.
695.
by creata 5y ago
`Functor` instances need to exist: they're obviously useful. You'll see a million `map` methods in every programming language.[0] What you won't see is a unification of them all under one interface. And the point, in my v
696.
by creata 5y ago
> To be honest I feel like the functor concept is too abstract and subtle to the point where it's probably not very useful in the context of programming. I think it's a small convenience to have the programming language automat
697.
by creata 5y ago
The one-letter variables are all type parameters, and pretty much every programming language uses one-letter variables for type parameters. And I can't think of a better syntax for "functions from a to b" than (a → b). In a
698.
by creata 5y ago
> You have 2 options: either your functions are recursive and you can hope and pray Or you can try to figure out the maximum number of times it'll recurse: for example, the height of a red-black tree with less than 2^64 nodes is les
699.
by creata 5y ago
> And at the end of the day understanding why cardinal is better than ordinal is not trivial to understand, unless you understand information encoding but that's not common knowledge (though it should be here and I'm surprised
700.
by creata 5y ago
I don't have a score in my head for each politician: I just know which are better, and which are worse. Consequently, > Most obviously, ranking is effectively a bubble sort, О(n^2), whereas rating is just two passes: 1. Get the max
701.
by creata 5y ago
I won't comment on the first link, but I don't buy that second link at all. Assuming that it's referring to the C code from elsewhere on their site[0] (boldly claimed to be 'the world's first "reality based&quo
702.
by creata 5y ago
I think you misread, but maybe I should've worded it more clearly: the silly people are those hypothetical people who say that "syntax doesn't matter" and "fewer characters means better syntax".
703.
by creata 5y ago
> it's ultimately subjective... and I don't have the energy this morning. Fair enough, but I've never seen anyone make either of the talking points that you claim are common, and they would be very silly things to say.
704.
by creata 5y ago
If you don't mind, what is it about the syntax of Dhall that you find hard? In my experience, Haskell's syntax is much simpler than the syntax of any of the popular languages. The "hard" parts of Haskell come with all th
705.
by creata 5y ago
> That's clearly using the language of set theory to talk about groups. If you like the language of set theory, what's wrong with replacing "A ⊆ X" with "A : SubsetOf X" where SubsetOf X = X → Prop? This is
706.
by creata 5y ago
> Modern mathematics textbooks, especially undergratuate ones, are written with set theoretic foundations. Yes, but only the foundations. A math undergrad doesn't actually care whether an ordered pair (a, b) is encoded as {{a},{a,
707.
by creata 5y ago
Maybe my imagination is too small, but what else could a solution look like? You want sequencing, and IO gives you exactly that.
708.
by creata 5y ago
It's not really important, but the "Grothendieck prime" is 57 according to Wikipedia. https://en.wikipedia.org/wiki/57_(number)#In_mathematics
709.
by creata 5y ago
This has to be the least charitable reading of Crazyontap's comment. Couldn't you have just inserted the implied: > I was just talking to a friend the other day on how badly Apple and Google are trying their best to kill curios
710.
by creata 5y ago
Reminds me of this line by tom_mellior[0]: > I wish people stopped approaching language design from the point of view that the people who have been working on garbage collection for the last 60 years are all idiots who don't see how
711.
by creata 5y ago
> We really do need to write an actual paper for Yatima's theory though Looking forward to it!
712.
by creata 5y ago
Who is grieving and what are they grieving about?
713.
by creata 5y ago
Some random questions to the developers regarding the motivation that "math is more fun when you have a computer to take care of the detail-work" [0]: 1. Do you have plans to make Yatima a usable theorem prover? 2. If so, how will
714.
by creata 5y ago
> i just remember how i was treated Pretty sure it's a personal recount.
715.
by creata 5y ago
Sorry, edited. I'm on Firefox 88.0.1, if that helps.
716.
by creata 5y ago
Minor bug: if I visit the page in 1920x1080, everything is too big. But if I resize the page to 960x1080 and back, the layout becomes good.
717.
by creata 5y ago
The author also has a HTML version of this tutorial at https://davidchristiansen.dk/tutorials/nbe/ using Racket instead of Haskell.
718.
Checking Dependent Types with Normalization by Evaluation [pdf](davidchristiansen.dk)
1 points by creata 5y ago|1 comments
719.
by creata 5y ago
Too late to edit, but: I'm an idiot, I was thinking of memory leaks, not use-after-free.
720.
by creata 5y ago
You don't need allocations to be part of the language, you just need destructors (or linear types.) But the Zig authors intentionally omitted destructors because they want all control flow to be explicit. There's more at [0]. Side

More ›