Typesafe Neural Networks in Haskell with Dependent Types | Hacker News Reader

Typesafe Neural Networks in Haskell with Dependent Types

blog.jle.im

140 pointsKirinDave18 comments

I didn't read this closely, but are those dependent types or just type-level integer literals? Can you use variables and/or arithmetic operations on the type index? If you can't instantiate the type with non-literals, then these aren't dependent types. Dependent types are types that depend on (i.e., the type constructors are functions of) actual values of the language, not types that are parameterized by other types (even if the syntax allows naming a type '42', which just looks like a value).

The series is about dependent types, it doesn't look like it's got as far as actual dependent types in part 1:

> what if we wanted to generate a network that has runtime-determined size (For example, getting the size from user input)? What if we wanted to load a pre-trained network whose size we don’t know? How can we manipulate our networks in a “dynamic” and generic way that still gives us all of the benefits of type-safe programming? We’ll found out next post!

GHC Haskell type-level Integer literals can constructed from non-literal just fine :)

https://hackage.haskell.org/package/base-4.7.0.2/docs/GHC-Ty...

There are type-level operators as well for arithmetic, but in my experience it’s a bit less pleasant than working with Peano Nats.

And can you say that a type is indexed by, say, an even number? How do you prove that?

With TypeLits, idk if that’s possible without some cheating. But that’s because (as the module name implies) these are type literals and mostly focused on having Integers that can go from type to term and vice-versa.

I can definitely do that with Singleton peano Nats pretty easily. I’ll end up with a function of type

  SNat n -> Maybe (IsEven n)

Where IsEven n is some structural proof of even-ness

  data IsEven (n :: Nat) where
    ZEven :: IsEven Z
    SEven :: forall (n ::Nat). IsEven n -> IsEven (S (S n))

I wrote this on my phone, but I’m sure it’s possible and kinda easy to work with at that.

A dependent type system needn't be able to express that a type is indexed by an even number. You can have dependent types without type-level computation, for example, by requiring that types be parameterized by nonexpansive expressions - which is nevertheless already more powerful than what Haskell's type system offers. This restriction might even be a good thing for type inference.

See https://blog.jle.im/entry/practical-dependent-types-in-haske... where you get this function definition: https://github.com/mstksg/inCode/blob/master/code-samples/de...

I liked this article: https://ren.zone/articles/safe-money where they get e.g. an ExchangeRate "USD" "JPY" type from input that has a different type from ExchangeRate "EUR" "JPY" (and thus can't be used to convert euros, only US dollars).

Agreed wholeheartedly. What this article shows is fundamentally no different from C++ templates manipulating `int`s (IOW, not dependent types), except for the richer selection of (promoted) data types.

Yet another step in the direction of bringing typed functional programming and machine learning together. Nice!

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.

>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 :)

> 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.

> 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).

r.e. "elevated heart rate".

really focusing on the meat of the article, eh?

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.

> But maybe the typical Haskell programmer is not a good enough mathematician, who knows.

Gloves off, boys and girls.

The next hoop to jump through would be to specify tape based autograd in a type system. The type system would not only have to specify the dimensions of the matrices, but the sequence of operations as well (in order to reverse them and perform the correct backprop sequence without relying on the runtime).

Slightly ignorant comment from a Haskell n00b - how does Agda play into this?

Reply on news.ycombinator.com