Comment by swatow | Hacker News Reader

Comment by swatow | Hacker News Reader

Parent Full thread

>Every year at my school I did exactly that. Once I actually turned in my solutions and my math teacher was quite upset because she didn't know what I'd do for the rest of the year in her class. She thought I was being arrogant and I should take in the material slowly, not swallow it all like a whale. But I wasn't arrogant or anything, because unfortunately this skill didn't transfer to the rest of my classes

Accusing people of being "arrogant" is a cheap way feel righteously indignant at the expense of someone smarter than you. I was fortunate enough to have some very nice teachers in grades 11-12, who complimented me on my intelligence and didn't try to take me down a notch for the sake of their own egos (nothing wrong with the teachers below grade 11, these issues just didn't come up as much at that time).

I studied mathematics as an undergrad, and later got into programming. Now I do machine learning as my job, and study dependently typed programming languages for fun. If you like mathematics I highly recommend Haskell and Idris (or Coq or Agda, but I found Idris them most approachable, as a programmer). In 50 years I think everyone will be using something dependently typed languages (or some other kind of language that is also fundamentally different to existing languages).

This is a bit of tangent, but I looked up Idris since I'd never heard of it. I'm currently learning Haskell and they look really similar. What differentiates the two? What can you do in one that you can't do in the other?

As practical matter, Idris is a new experimental language while Haskell is a mature, stable language with a useful standard library.

But fundamentally Idris is theoretically more advanced than Haskell. The core differences are

1. Idris functions can be proven to terminate (if you choose).

2. In Idris, types are first class values, and you can have dependent functions: functions whose return type depends on their input value.

An example of something you can do in Idris and not* in Haskell, in Idris you can define a vector type Vect n a, which is the type of vectors of length n with values in type a. You can also define Fin n, the set of integers less than n. Then you can define a function index : Fin n -> (Vect n a) -> a which takes an integer less than n, a vector of length n with element of type a, and returns an element of type a. This function is guaranteed to return a value, because the index is guaranteed to be in the correct range.

*For some meaning of "not": you can probably do this in some way in Haskell.

Yeah, you can definitely do that example in Haskell – if by Haskell you mean GHC. GHC has been slowly but surely adding dependently-typed features for quite some time now, which will culminate in a proper DependentTypes pragma sometime soon (for some meaning of soon, anyway).

There are a lot of other differences between Haskell and Idris, though. Totality is a pretty big thing, and Idris is also strict by default. It also has support for proof tactics, which I don't see Haskell getting anytime soon.

I'm somewhat new to the field, so this might not be properly phrased, but isn't totality an inherent part of full dependent types?

I'm not an expert, but I wouldn't think so. To me, full dependent types just means you have pi and sigma types. I don't see anything fundamental about pi and sigma types that would prevent you from having bottom in your language, or from allowing users to define partial functions.

Although I am not expert on these things but it seems to me that Idris has better support for so called dependent types http://ejenk.com/blog/why-dependently-typed-programming-will...

This was an interesting read. Thanks for sharing!

> This means that whenever I call this function, I need to provide together with a and b a proof that b isn’t zero.

What might such a proof look like? And is this supposed to work at compile-time?

Yes, it happens at compile time. To understand how proofs work here, you want to look at the Curry-Howard correspondence. Basically, there's a correspondence between types and propositions, and between the values inhabiting those types and proofs of the corresponding propositions. So a proof looks like a value of a certain type.

Reply on news.ycombinator.com