TheAsprngHacker

11 ms·

61.
by TheAsprngHacker 7y ago
What Python and other dynamically typed languages call "types" aren't types at all in the theoretical sense. In type theory, types are properties ascribed to programs that describe their behavior and are part of a language&#x
62.
by TheAsprngHacker 7y ago
Ltac2 in the documentation: https://coq.inria.fr/distrib/current/refman/proof-engine/lta...
63.
Coq 8.11.0 released, featuring new Ltac2 tactic language(github.com)
1 points by TheAsprngHacker 7y ago|1 comments
64.
by TheAsprngHacker 7y ago
Have you heard of the Curry-Howard correspondence [0]? This states that a type system is actually a logical system. The types are propositions (logical statements) and their terms (the expressions of that type) are proofs. It's a strai
65.
by TheAsprngHacker 7y ago
Agda and GHC Haskell have a feature called "typed holes" that can enhance the workflow that you describe in the article. If you're not sure how to finish a definition, you can leave a "hole" in the expression where
66.
by TheAsprngHacker 7y ago
Are you referring to how an online document or a file might change so that Haskell program might have a different output given the same URL as an input? As @willtim explains, monads were applied to PL theory to model effects. The IO monad m
67.
by TheAsprngHacker 7y ago
I think it looks okay.
68.
by TheAsprngHacker 7y ago
For what it's worth, despite the O in OCaml, in practice the object layer isn't used that often. However, that's because the ML module system serves many of the same use cases that objects and classes do in other languages. P
69.
by TheAsprngHacker 7y ago
I am not a moderator, but if you prefix your submission with "Show HN: " then it will appear on the Show HN tab: https://news.ycombinator.com/show This page is designated for people to show off their projects. You
70.
by TheAsprngHacker 7y ago
As someone who isn't familiar with this Lisp dialect / DSL, something that stands out to me is the (def-struct ...) ... (def-struct-end), (def-method ...) ... (def-func-end), (switch) ... (endswitch), and (vpif ...) ... (endif). T
71.
by TheAsprngHacker 7y ago
A blog that I recently discovered is the Sakuga Blog, which analyzes the process of anime production, the works of individual animators, and the state of the anime industry. The blog is very nuanced and has led me to better appreciate the a
72.
by TheAsprngHacker 7y ago
Since hyperlinks can link to any document, not just children, shouldn't the data structure be a (not necessarily tree-shaped) directed graph?
73.
by TheAsprngHacker 7y ago
Hmm, why isn't this showing up on Ask HN tab? Someone else submitted an Ask HN right after mine, and that one's showing up on the Ask HN tab.
74.
Ask HN: I got rejected from Cornell. I want to study PL theory; what to do?
1 points by TheAsprngHacker 7y ago|6 comments
75.
by TheAsprngHacker 7y ago
> You can count the number of type systems that are "logically OK" (the formal terms are sound (doesn't admit wrong programs, unlike e.g. Java), complete (can admit all correct programs (for some definition of "co
76.
by TheAsprngHacker 7y ago
I use OCaml, and monads also come up in OCaml code. Monads may not be as essential to understand in OCaml than in Haskell because OCaml doesn't use them to track IO in the type system, but people use them in OCaml to chain options and
77.
by TheAsprngHacker 7y ago
If you're new to functional programming, you don't need to worry about the category theory definition. Especially since this tutorial simply mentions it as a way to say, "this is too complicated for us, so we're going to
78.
by TheAsprngHacker 7y ago
The ML family and Haskell are good for writing compilers because sum types and pattern matching lend themselves well to ASTs and symbolic manipulation. OCaml and Haskell have been used for real-world language projects (OCaml is used to impl
79.
by TheAsprngHacker 7y ago
Discussion on r/math: https://www.reddit.com/r/math/comments/dzbmbu/a_new_way_to_s...
80.
A New Way to Solve Quadratic Equations – Po-Shen Loh(poshenloh.com)
1 points by TheAsprngHacker 7y ago|1 comments
81.
by TheAsprngHacker 7y ago
In my code, the Z doesn't mean integer; it stands for zero. Nat is an inductive type, and Z is the base case. Z has type Nat.
82.
by TheAsprngHacker 7y ago
> There's no ADT in category theory. The only place you might find them is in type theory I wouldn't say that this is true. Category theory has a definition of product of objects, sum/coproduct of objects, terminal object
83.
by TheAsprngHacker 7y ago
First, here is a note about the notation that I will use here: Let `1` denote the unit type, the type with one inhabitant. Let `()` denote the inhabitant of the unit type. Let `a + b` or `Either a b` denote the sum of types `a` and `b`. Let
84.
by TheAsprngHacker 7y ago
Hmm, why isn't this appearing on the Ask HN page?
85.
Ask HN: What are the security and legal aspects of websites with user content?
2 points by TheAsprngHacker 7y ago|1 comments
86.
by TheAsprngHacker 7y ago
Huh? A monad isn't a sealed class, it's a generic type equipped with the functions bind and return...
87.
by TheAsprngHacker 7y ago
The fact that the name "Yuri" is on this list is interesting because "Yuri" is both a masculine Slavic name and a feminine Japanese name. The rapid switch could be due to the growth or decline of one of these names, wher
88.
by TheAsprngHacker 7y ago
As a disclaimer, I do not believe I've ever seen a captcha when logging in to GitLab. But according to https://docs.gitlab.com/ee/integration/recaptcha.html , you use reCAPTCHA? Are you aware of the privacy co
89.
by TheAsprngHacker 7y ago
I'm very confused about what this blog post is trying to argue. Most of what it discusses isn't related to the Curry-Howard correspondence at all? At the risk of sounding anti-intellectual, perhaps Orwell's "Politics and
90.
by TheAsprngHacker 7y ago
To be honest, I didn't know about the RAML you link until I read your comment. Would this RAML be common knowledge for people who aren't web developers / don't regularly use web APIs?

More ›