Danny Gratzer writes about type theory, functional programming, Haskell, ML modules, and compilers.
HN commenters cite it for explanations of ML modules and dependent types, and for its post advising Haskell learners not to start with category theory.
> Go model a square and a rectangle in your favorite statically typed language.
Okay.
data Shape = Square Int | Rectangle Int Int deriving (Show)
> You will find that square extends rectangle and setting the length on a square also sets the width.
Why? I don't really see a need for square to extend a rectangle.
> So if I have a collection of rectangles which contains an unknown number of squares of which I set the width on each of them.
Like this?
> let unknowns = [(5,4),(3,2),(4,4)]
> let toShape (x,y) = if x == y then Square x else Rectangle x y
> map toShape unknowns
[Rectangle 5 4,Rectangle 3 2,Square 4]
Tomorrow I'll see if I can make this type-safe by using dependent typing as shown in: [0][1][2]
This was easily solvable in my staticly typed language as you can see. In something like Idris I could have
very easily encoded the toShape function the the type signature.
0: http://www.alfredodinapoli.com/posts/2014-10-13-fun-with-dependent-types-in-haskell.html
1: https://www.fpcomplete.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell
2: http://jozefg.bitbucket.org/posts/2014-08-25-dep-types-part-1.html
Coming from an SML background, one of the things that's always tripped me up about Haskell is that it doesn't have structures, signatures, and functors for grouping code. Instead it has modules, which are not much more than groups of exported functions.
For Haskellers coming to SML, there's "A Crash Course on ML Modules"[1] which does a nice job of explaining things in the opposite direction.
Are there any resources like this out there that discuss how best to break down and write modular Haskell programs?
[1]: http://jozefg.bitbucket.org/posts/2015-01-08-modules.html
(update: I realized the original article I linked to wasn't the one I thought it was!)
> Everybody who does PL theory more seriously probably knows that, but I didn't realize how close type inference and prolog-like systems look.
Yup! This is more to do with a very specific part of type theory - ie. 'type reconstruction' (more commonly referred to as 'type inference'). One of the most notable examples of this is the so-called 'Hindley-Milner type system' which can be proven to decidable. Here is a good explanation of the constraint-solving algorithm: http://jozefg.bitbucket.org/posts/2015-02-28-type-inference.html
The use of the term "witness" here comes from constructive logic, where proofs of propositions have actual computational content. There "witness" means the same thing as "proof" but is more evocative that the proof is data that can actually be manipulated.
You might like this article if you're interested to learn more: http://jozefg.bitbucket.org/posts/2015-01-09-constructivism.html
> If you want to learn Haskell, forget Category theory
Yes please. Please Don't Learn Category Theory to Learn Haskell: http://jozefg.bitbucket.org/posts/2013-10-14-please-dont-learn-cat-theory.html
> learning category theory will likely help you learn Haskell about as much as learning lambda calculus will help you learn Lisp. Maybe a bit less
Much, much less, I would have said
I like how he wrote a post a few days later, Learn You Some Category Theory:
http://jozefg.bitbucket.org/posts/2013-10-22-category-theory-in-haskell.html