TheAsprngHacker

8 ms·

31.
by TheAsprngHacker 6y ago
For the record: I am a high school senior who learned about type theory in my free time. When I make this comment, I do not mean to boast, and I did invest a lot of time into learning TT. It's a coincidence, because I was just reading
32.
by TheAsprngHacker 6y ago
I think there's perhaps an analogy to be made between FP terminology that comes from math, and is therefore unfamiliar to non-math people, and type theory notation such as this. For example, an FP "functor" comes from the ide
33.
by TheAsprngHacker 6y ago
Discussion on r/ProgrammingLanguages: https://www.reddit.com/r/ProgrammingLanguages/comments/gg0cm...
34.
by TheAsprngHacker 6y ago
To my understanding skimming the paper, the analysis must compute "call contexts" of functions, which use information from call sites. I wonder if this will impede incremental compilation and modularity. As programs get bigger, pe
35.
by TheAsprngHacker 6y ago
Discussion on r/ProgrammingLanguages: https://www.reddit.com/r/ProgrammingLanguages/comments/gfgn0... Discussion on r/rust: https://www.reddit.com/r/rust/comments/gfgt
36.
Sharing Joel David Hamkins’s “almost correct proofs” tweet with my son(mikesmathpage.wordpress.com)
2 points by TheAsprngHacker 6y ago|0 comments
37.
by TheAsprngHacker 6y ago
Mark Liberman is the professor mentioned in this recent thread: https://news.ycombinator.com/item?id=22975907
38.
by TheAsprngHacker 6y ago
This is the associated course: https://pl.cs.jhu.edu/pl/index.shtml This is Part II of the course: https://pl.cs.jhu.edu/pl2/index.shtml
39.
Principles of Programming Languages [JHU Textbook] [PDF](pl.cs.jhu.edu)
3 points by TheAsprngHacker 6y ago|1 comments
40.
by TheAsprngHacker 6y ago
Wow, cool! I'm still wrapping my head around Cubical Type Theory, so I'm not sure if I can help. I don't have the mathematical background to know what Matroids are (skimming the Wikipedia page, I see some set-theory-centric d
41.
by TheAsprngHacker 6y ago
Do you have any project ideas for Agda? I used it to formalize the simply typed lambda calculus; what else should I do? After all, I can't really do "traditional" programming projects in Agda as its ecosystem is more geared t
42.
by TheAsprngHacker 6y ago
Sorry, by "untyped" I meant "dynamically typed." CL does have a sophisticated type hierarchy, but to my knowledge, according to the standard, types are checked at runtime, right? In the type-theoretic sense, "type&q
43.
by TheAsprngHacker 7y ago
Hi, maybe this is offtopic, but I felt this way when anime studio KyoAni was arsoned and many of its employees died in a horrific way, and the news got to the front page of HN: https://news.ycombinator.com/item?id=20468395
44.
by TheAsprngHacker 7y ago
Care to explain why, for someone who hasn't used this tool?
45.
by TheAsprngHacker 7y ago
This is a list of type theory resources: https://github.com/jozefg/learn-tt This is an exposition of Martin-Lof's dependent type theory: http://www.cs.nott.ac.uk/~psztxa/mgs-17/notes-mgs1
46.
by TheAsprngHacker 7y ago
Given that most (but not all) Lisps are untyped, I don't see what Lisp evangelism has to do with the Curry-Howard correspondence...
47.
Verified Functional Programming in Agda(dl.acm.org)
88 points by TheAsprngHacker 7y ago|10 comments
48.
by TheAsprngHacker 7y ago
I was going to comment this, but you got here before me. So, I would just like to ramble about type theory and constructive logic a bit. According to the Curry-Howard correspondence and the BHK interpretation of logic, there is a syntactic
49.
by TheAsprngHacker 7y ago
Here is a list of Snap! extensions if they are of any use to you as references: https://snap.berkeley.edu/extensions Scratch 3 runs on a modified version of Blockly.
50.
by TheAsprngHacker 7y ago
The Snap! mascot is named Alonzo after Alonzo Church, and the "horn" is a lambda to symbolize Snap!'s functional programming features. I just checked, and both Alonzo and Gobo have three feet. "Sprite" and "cos
51.
by TheAsprngHacker 7y ago
Snap! is explicitly based on Scratch and started out as a fork, BYOB. Snap! was rewritten from the ground up. Snap!'s motto is "First class everything," and taking inspiration from Scheme, it supports first-class lists, first
52.
by TheAsprngHacker 7y ago
Funnily, in programming languages based on Martin Lof Type Theory, the topic of function extensionality is a whole rabbit hole for reasons other than the halting problem. There is a distinction between intensional Martin Lof type theory and
53.
by TheAsprngHacker 7y ago
I'm using OCaml to make my own programming language. OCaml is good for programming language implementation because algebraic data types + pattern matching lend themselves naturally to AST manipulation. I also like OCaml because it is b
54.
by TheAsprngHacker 7y ago
It look like this is your own project. If you prefix the title of this submission with "Show HN:", then it will appear under the "show" tab and you will get more visibility.
55.
by TheAsprngHacker 7y ago
Why do people credit the pipe operator to F#? OCaml has it too, and F# is based on OCaml. Did the pipe operator get added to F# first? (The OCaml docs say that the pipe operator first appeared in OCaml 4.01 [1], and I can't find out wh
56.
Naoko Yamada: Filmed with the Heart(blog.sakugabooru.com)
1 points by TheAsprngHacker 7y ago|0 comments
57.
by TheAsprngHacker 7y ago
Coq 8.11.0 was recently released: https://github.com/coq/coq/releases/tag/V8.11.0 This version introduces a new tactic language, Ltac2.
58.
by TheAsprngHacker 7y ago
> applicative -> equivalent of turning one element into a list This is only one part of the definition of an applicative. Applicatives must also preserve the monoidal operation (product). That is, there is a function `pair : f a ->
59.
by TheAsprngHacker 7y ago
Oops, thanks.
60.
by TheAsprngHacker 7y ago
But "apply a function to every object in a list" isn't the definition that the author is getting at! Most programmers probably know "map" as being an operation takes a function and a list and returns a list of the

More ›