TheAsprngHacker

15 ms·

91.
by TheAsprngHacker 7y ago
Agreed, and Scratch is hardly the pinnacle of programming language theory. I was talking to professor Shriram Krishnamurthi a week ago about a block-based, educational ML dialect I was making, and he told me that he believed that once a lan
92.
by TheAsprngHacker 7y ago
Calling it topology can be misleading, as HoTT only considers types as spaces in the sense of homotopy equivalence.
93.
by TheAsprngHacker 7y ago
Homotopy Type Theory is based on Martin-Lof Type Theory (which is your standard dependent type theory), but reinterprets equality to mean homotopy equivalence. In vanilla MLTT, a = b is inhabited iff a and b share the same normal form, and
94.
by TheAsprngHacker 7y ago
As someone who's never used Lean, but has played around with Coq and Agda, how do they compare?
95.
by TheAsprngHacker 7y ago
The ML programming language is known for its advanced module system. First, you have structured, which are your traditional idea of a module. Structures define types and data. Signatures describe the interface of a module and are like the m
96.
by TheAsprngHacker 7y ago
The OCaml type 'a * 'b is the equivalent of the Haskell type (a, b). This type is known as the Cartesian product type, and it's written with a multiplication symbol in type theory (hence the asterisk in OCaml syntax). The pro
97.
by TheAsprngHacker 7y ago
Thank you for pointing out contravariant functors; I have fixed that sentence in my post and credited you.
98.
by TheAsprngHacker 7y ago
I can try to explain this to you from a math perspective, if you want, but I need to know your math background. Are you familiar with the lambda calculus and its relationship to category theory?
99.
by TheAsprngHacker 7y ago
The other person also mentioned this. It's called invariance. There's also a fourth variance: https://www.benjamin.pizza/posts/2019-01-11-the-fourth-type-...
100.
by TheAsprngHacker 7y ago
Isomorphism is not about currying. When I mentioned isomorphism, I was referring to the interchangeability in general, and the currying relationship is just an example of an isomorphism. In category theory notation: Hom(A * B, C) ~ Hom(A,
101.
by TheAsprngHacker 7y ago
Thank you for the praise. For me, the inline code has about the same font size as the surrounding text, maybe smaller, and the block code has a bigger font. Is it possible for you to send me a screenshot? I'm a little confused by your
102.
by TheAsprngHacker 7y ago
In your opinion, is this article less helpful than the functor/monad tutorials that predominantly use Haskell?
103.
by TheAsprngHacker 7y ago
Thanks. I know what contravariant functors are, but I haven't used them, so I didn't realize that was what the parent commenter was asking about. You're right, my claim that every type 'a t has a corresponding (covariant
104.
by TheAsprngHacker 7y ago
If there is a function `map : ('a -> 'b) -> 'a t -> 'b t`, and there exists a function `x : 'w -> bool`, then `map x : `'w t -> bool t`. Is this what you were asking?
105.
by TheAsprngHacker 7y ago
Huh? I cover this definition in the tutorial, when I discuss OCaml's (and+) operator! Did I gloss over things too quickly?
106.
by TheAsprngHacker 7y ago
Shrugs Well, Python is dynamically typed and C doesn't really have good polymorphism or first-class function support. Both polymorphism and first-class functions (with closures) are important for understanding functors, applicatives,
107.
by TheAsprngHacker 7y ago
The majority of my tutorial actually uses OCaml, though. :P I like OCaml because it strikes a balance between imperative and functional programming. Maybe learning OCaml would be easier than learning Haskell? (Plus, OCaml has neat features
108.
by TheAsprngHacker 7y ago
To my understanding, although the behaviors of filterM, etc. differ depending on the monad instance, as long as the monad instances follow the laws, those functions like filterM have predictable behavior. It's a consequence of "
109.
by TheAsprngHacker 7y ago
I am the author of this submission. I have strong opinions about functor and monad tutorials, and here are my thoughts: Back when I didn't understand what a monad was, I would read a bunch of tutorials and get confused by the analogies
110.
Functor, Applicative, and Monad(typeslogicscats.gitlab.io)
252 points by TheAsprngHacker 7y ago|120 comments
111.
by TheAsprngHacker 7y ago
See also literate programming, in which the source code is contained inside some kind of prose and the entire file is a valid program: https://en.wikipedia.org/wiki/Literate_programming It seems that the computational
112.
by TheAsprngHacker 7y ago
I think that the parent commenter was being sarcastic to ridicule people who think that there being one cold winter day means that global warming isn't real.
113.
by TheAsprngHacker 7y ago
I already submitted this: https://news.ycombinator.com/item?id=20912460 P.S. Are you the same person who submitted this on Reddit?
114.
by TheAsprngHacker 7y ago
This is the source: https://github.com/SOSML/SOSML Standard ML (SML) is a typed functional programming language from the ML family (the same family that OCaml is from). SML doesn't seem to receive the same spotlig
115.
SOSML – Online Standard ML Interpreter(sosml.github.io)
1 points by TheAsprngHacker 7y ago|1 comments
116.
by TheAsprngHacker 7y ago
ELI5: Constructive math is a philosophy of math where you must construct a value to proof its existence. The Intermediate Value Theorem states that if f(a) < 0 and f(b) > 0, then there exists a number c in the interval (a, b) where
117.
Why Isn't the Intermediate Value Theorem Constructive?(math.stackexchange.com)
1 points by TheAsprngHacker 7y ago|1 comments
118.
by TheAsprngHacker 7y ago
I am the author of this post, please ask me any questions. Reddit discussion: https://www.reddit.com/r/programming/comments/cy35zz/functor... My HN submission (which didn't receive any traction): h
119.
Functor, Applicative, and Monad(typeslogicscats.gitlab.io)
1 points by TheAsprngHacker 7y ago|0 comments
120.
by TheAsprngHacker 7y ago
I personally don't use Reason. It's syntax is supposed to be more familiar for people coming from JavaScript, but for me, it's weird. My least favorite aspect is the function syntax (both lambdas and function application). Ar

More ›