Comment by dragonwriter | Hacker News Reader

Comment by dragonwriter | Hacker News Reader

Parent Full thread

> Why he hell does this sequence of characters "data Nat = Z | S Nat" define a natural number?

Because a natural number is either zero (the one value of type Z, which has a nullary type constructor and therefore only one value) or (represented by the vertical bar "|") the successor to another natural number (represented by type S, which has a one-arg constructor whose argument is of type Nat.) Its a recursive type definition, with a base case and a recursive case.

> It would be good to have an introduction for people not too familiar with functional languages.

It would be; right now, you are probably be best served by one of the ones for Haskell -- Idris doesn't seem to have a lot of documentation not aimed at people not already familiar with functional programming, and really familiarity with Haskell seems to be the most applicable to Idris.

The Idris tutorial [1] assumes familiarity with Haskell, but does provide brief descriptions of the relevant syntax which may be enough.

[1] http://eb.host.cs.st-andrews.ac.uk/writings/idris-tutorial.p...

While it's mathematically conventional and maybe event elegant to represent integers that way, isn't it ridiculously inefficient to actually implement it that way? I guess there is going to be something in the compiler that recognizes and special-cases this pattern, but still...

Also, I really wonder why there is no language with "nice"/"conventional"/C/ALGOL/... syntax for dependent types. Right now my dream language would be something like Spec# (which is C# with contracts), but it would try to prove its contracts (within the bounds of possibility of course, wrt. the halting problem and so on).

> While it's mathematically conventional and maybe event elegant to represent integers that way, isn't it ridiculously inefficient to actually implement it that way?

It would be, but the compiler recognizes the pattern and does ordinary integer arithmetic where it needs to (the pattern is relevant, however, to the use of individual natural numbers in defining other types, which is pretty important to Idris.)

> Also, I really wonder why there is no language with "nice"/"conventional"/C/ALGOL/... syntax for dependent types.

I don't think C/ALGOL-style syntax is all that nice when it comes to even Haskell's level of typing, much less dependent types.

That said, if dependent typing takes off, no doubt we'll see languages that fuse it with C-style syntax soon after, just as we saw with OOP and basically every other thing since.

> It would be, but the compiler recognizes the pattern and does ordinary integer arithmetic where it needs to (the pattern is relevant, however, to the use of individual natural numbers in defining other types, which is pretty important to Idris.)

The compiler does recognise it, because it'd be silly not to, but more importantly, Nats tend to be type level things which explain the structure of something else (e.g. a successor corresponds to a cons, or to another level in a tree), and as such don't appear in runtime code anyway. If what you want is machine arithmetic, better to use a type that's designed for that.

Idris has Haskell-like syntax because I like Haskell style syntax (this is probably the most important reason!) and Haskell programmers are the initial target audience.

I recently stumbled on something called "view", a concept implemented in the Hope language. For those not familiar with it, it let you define bijections between 2 different datatypes, so that one may pattern match a piece of data from one datatype with the other datatype constructors, and one of the examples in the paper was precisely that correspondence between peano numbers and usual (unsigned) integers (well, really, it's not quite bijective, given the arch limits on integer representation, but for any purposes we can think of yet, it works). So, the question is: is idris using something like that? Or is there another mechanism? Is it a builtin feature of the language? Do you use the proof system to persuade the language kernel it may translate them back and forth (the "software foundation" book for Coq let the reader build a few proofs about that, though Coq use arbitrary precision numbers iirc))? I'm still quite new on dependent typing, so forgive me if this question is silly or weird somehow.

>That said, if dependent typing takes off, no doubt we'll see languages that fuse it with C-style syntax soon after, just as we saw with OOP and basically every other thing since.

Indeed, type systems for (actual) Javascript are often formulated in terms of dependent types.

Do you have a reference on that? I'd love to read it

http://goto.ucsd.edu/~ravi/research/oopsla12-djs.pdf

Thanks!

Reply on news.ycombinator.com