5 ms·

Very good example and motivation for dependent types. However, I think it makes strange assumptions on its readership. For example: > If you’re a non-Haskell

by vog 9y ago

Very good example and motivation for dependent types. However, I think it makes strange assumptions on its readership. For example: > If you’re a non-Haskell programmer, this might all seem perfectly fine and normal, and you probably have only a slightly elevated heart rate. If you are a Haskell programmer, you are most likely already having heart attacks. Well, for a non-Haskell programmer, the Haskell code snippets make very few sense, simply because they are not used to the syntax. And those non-Haskell programmers who are used to the ML-syntax are programming in SML, OCaml or F#, which all have a similar type system to Haskell's, and hence do get "elevated heart rate". If this article is really meant to be readable by non-Haskell programmers, the example code snippets should also be provided in a more mainstream language with static types, such as C++, Java or perhaps JavaScript+TypeScript.

Tehnix 9y ago
>Well, for a non-Haskell programmer, the Haskell code snippets make very few sense, simply because they are not used to the syntax I didn't take that remark to be anything about the syntax, but rather how unsafe the code is, since we are dealing with matrices that have assumptions on their dimensions, essentially leaving the bugs for runtime — he follows this up with several bullet points explaining why the heart attack :)
- vog 9y ago
  > I didn't take that remark to be anything about the syntax Exactly that's the problem: The author is ignoring the syntax issue, that is, the fact that the vast majority of non-Haskell programmers won't be able to make much sense of the the code examples.
platz 9y ago
r.e. "elevated heart rate". really focusing on the meat of the article, eh?
catnaroek 9y ago
I program in Standard ML everyday, and I don't get an “elevated heart rate” when I see something that can't be proved with a type checker. I just prove it by hand. But maybe the typical Haskell programmer is not a good enough mathematician, who knows.
- tome 9y ago
  > But maybe the typical Haskell programmer is not a good enough mathematician, who knows. Gloves off, boys and girls.
thinkpad20 9y ago
> If this article is really meant to be readable by non-Haskell programmers, the example code snippets should also be provided in a more mainstream language with static types, such as C++, Java or perhaps JavaScript+TypeScript. First of all, the definition of "readable by non-Haskell programmers" will always be somewhat subjective. Depending on their background, aptitude and motivation, many non-Haskell programmers can understand Haskell code just fine. Setting that aside, the techniques described in this blog post simply wouldn't be possible to express in any of those languages. Just having static types is not sufficient. Even in vanilla Haskell, most type-level programming techniques are not possible to express, and certainly the type systems of Java etc are not capable of it (without significant extension).

by vog 9y ago

Tehnix 9y ago

>Well, for a non-Haskell programmer, the Haskell code snippets make very few sense, simply because they are not used to the syntax I didn't take that remark to be anything about the syntax, but rather how unsafe the code is, since we are dealing with matrices that have assumptions on their dimensions, essentially leaving the bugs for runtime — he follows this up with several bullet points explaining why the heart attack :)

vog 9y ago
> I didn't take that remark to be anything about the syntax Exactly that's the problem: The author is ignoring the syntax issue, that is, the fact that the vast majority of non-Haskell programmers won't be able to make much sense of the the code examples.

platz 9y ago

r.e. "elevated heart rate". really focusing on the meat of the article, eh?

catnaroek 9y ago

I program in Standard ML everyday, and I don't get an “elevated heart rate” when I see something that can't be proved with a type checker. I just prove it by hand. But maybe the typical Haskell programmer is not a good enough mathematician, who knows.

tome 9y ago
> But maybe the typical Haskell programmer is not a good enough mathematician, who knows. Gloves off, boys and girls.

thinkpad20 9y ago

> If this article is really meant to be readable by non-Haskell programmers, the example code snippets should also be provided in a more mainstream language with static types, such as C++, Java or perhaps JavaScript+TypeScript. First of all, the definition of "readable by non-Haskell programmers" will always be somewhat subjective. Depending on their background, aptitude and motivation, many non-Haskell programmers can understand Haskell code just fine. Setting that aside, the techniques described in this blog post simply wouldn't be possible to express in any of those languages. Just having static types is not sufficient. Even in vanilla Haskell, most type-level programming techniques are not possible to express, and certainly the type systems of Java etc are not capable of it (without significant extension).