7 ms·

Idris - pure functional programming language with dependent types

74 points by alrex021 15y ago

mindcrime 15y ago
Is this, by any chance, specifically tailored to programming control systems for time machines[1]? [1]: http://tardis.wikia.com/wiki/Idris http://tardis.wikia.com/wiki/Idris
phaer 15y ago
Down for me, google cache: http://webcache.googleusercontent.com/search?q=cache:dtmf_mGqwA4J:idris-lang.org http://webcache.googleusercontent.com/search?q=cache:dtmf_mG...
- edwinb 15y ago
  Sorry about that, it's back now...
DanWaterworth 15y ago
This looks really cool. I haven't looked into dependently typed languages in depth, but this is the first one I've seen that looks like a programming language to write programs in.
skrebbel 15y ago
I love the concept, but the tutorial somewhat puts me off (admission: I only read the first third). I mean, using an "element from a finite set" to index a vector? Back home, we use natural numbers for that. Idris also has natural numbers, but somehow we still have to, essentially, use the "finite set of values we don't care about, but that we can order if we want to since, after all, the set has a finite number of elements" concept for what's essentially an array lookup. Why can't there be a type of "natural numbers under N"? Or am I all misunderstanding things, and is the "finite set" exactly that type, just explained in a very not straight forward way? Also, impressively, the author claims it has C-style speed. Does that mean that looking up a value in a vector by means of an element in a finite set is actually translated to a single *(vect+index)? (in C-terms)
- edwinb 15y ago
  That is indeed exactly what Fin is. The first n natural numbers is a finite set of n elements after all. I'll elaborate a bit in the tutorial. I guess the trouble with writing a tutorial when you're completely familiar with a language is that it's hard to know what will and won't make sense! There'd also be nothing wrong to use a natural number, along with a proof that it's bounded by the length, to index the vector. I don't think I've claimed it has C-style speed anywhere. At least, not in general - we have observed it in some cases though, and it is a goal to make it as efficient as possible. Dependent types plus partial evaluation gives you some nice opportunities for optimisation. Early days yet...
  - skrebbel 15y ago
    That is indeed exactly what Fin is. The first n natural numbers is a finite set of n elements after all. Ah, right! I must admit that it feels like an odd definition to me indeed. I see how "the first n natural numbers" is a finite set of n elements, but I don't see how the reverse is true. I mean, look here, a finite set of n elements: {1, 1, 1, 1}. 4 elements, and they're all valued 1. They're also not ordered. So your concept of taking an element from a finite set (in this case, let's say, 1, or maybe 1 instead) to uniquely identify an element in a vector sounds a bit odd to me :-) Clearly, I'm the noob here, and maybe in this stage Idris just isn't meant for people not on Lambda the Ultimate, but if not, it's good that you intend do something about it :-) Cause once again, I love the concept, and I'd love to program with this.
    - fhars 15y ago
      The set {1, 1, 1, 1} has only one element, 1.
      - skrebbel 15y ago
        Oh fuck. Bags and sets. I'm an idiot! And that only 3 years out of university :-(
- batterseapower 15y ago
radarsat1 15y ago
Very nice, haven't heard of this before. I think an ideal target for a dependently typed language is scientific array programming, so that you can ensure the sizes of your matrix and array operations check out before performing long-running tasks. If a good array library can be built (e.g. port Haskell's Repa) then it might provide a great foundation for this.
- dons 15y ago
  With type level naturals recently added to GHC, statically checked arrays are already implementable in Haskell. * http://hackage.haskell.org/package/vector-static http://hackage.haskell.org/package/vector-static * http://hackage.haskell.org/package/hmatrix-static http://hackage.haskell.org/package/hmatrix-static A nice next step would be to optimize out additional runtime bounds checks.
  - radarsat1 15y ago
    Very nice! I really look forward to using something like that.
amatus 15y ago
Am I correct in my understanding of these types? Vect a n = vector of a with known length n (n ** Vect a n) = vector of a with unknown length n When I think of it this way it's obvious why filter takes a Vect and returns a pair. Though it seems ugly to have to write each vector function to take both "static" and "dynamic" vectors.
- edwinb 15y ago
  That's right. You don't normally need to write each vector function both ways. If you can statically know the length (which you normally do in practice, at least in my experience) then you can write down a more precise type. filter serves as an example of what you might do when you need to compute an index dynamically.

74 points by alrex021 15y ago

Is this, by any chance, specifically tailored to programming control systems for time machines[1]? [1]: http://tardis.wikia.com/wiki/Idris http://tardis.wikia.com/wiki/Idris

phaer 15y ago

Down for me, google cache: http://webcache.googleusercontent.com/search?q=cache:dtmf_mGqwA4J:idris-lang.org http://webcache.googleusercontent.com/search?q=cache:dtmf_mG...

edwinb 15y ago
Sorry about that, it's back now...

DanWaterworth 15y ago

This looks really cool. I haven't looked into dependently typed languages in depth, but this is the first one I've seen that looks like a programming language to write programs in.

skrebbel 15y ago

I love the concept, but the tutorial somewhat puts me off (admission: I only read the first third). I mean, using an "element from a finite set" to index a vector? Back home, we use natural numbers for that. Idris also has natural numbers, but somehow we still have to, essentially, use the "finite set of values we don't care about, but that we can order if we want to since, after all, the set has a finite number of elements" concept for what's essentially an array lookup. Why can't there be a type of "natural numbers under N"? Or am I all misunderstanding things, and is the "finite set" exactly that type, just explained in a very not straight forward way? Also, impressively, the author claims it has C-style speed. Does that mean that looking up a value in a vector by means of an element in a finite set is actually translated to a single *(vect+index)? (in C-terms)

edwinb 15y ago
That is indeed exactly what Fin is. The first n natural numbers is a finite set of n elements after all. I'll elaborate a bit in the tutorial. I guess the trouble with writing a tutorial when you're completely familiar with a language is that it's hard to know what will and won't make sense! There'd also be nothing wrong to use a natural number, along with a proof that it's bounded by the length, to index the vector. I don't think I've claimed it has C-style speed anywhere. At least, not in general - we have observed it in some cases though, and it is a goal to make it as efficient as possible. Dependent types plus partial evaluation gives you some nice opportunities for optimisation. Early days yet...
- skrebbel 15y ago
  That is indeed exactly what Fin is. The first n natural numbers is a finite set of n elements after all. Ah, right! I must admit that it feels like an odd definition to me indeed. I see how "the first n natural numbers" is a finite set of n elements, but I don't see how the reverse is true. I mean, look here, a finite set of n elements: {1, 1, 1, 1}. 4 elements, and they're all valued 1. They're also not ordered. So your concept of taking an element from a finite set (in this case, let's say, 1, or maybe 1 instead) to uniquely identify an element in a vector sounds a bit odd to me :-) Clearly, I'm the noob here, and maybe in this stage Idris just isn't meant for people not on Lambda the Ultimate, but if not, it's good that you intend do something about it :-) Cause once again, I love the concept, and I'd love to program with this.
  - fhars 15y ago
    The set {1, 1, 1, 1} has only one element, 1.
    - skrebbel 15y ago
      Oh fuck. Bags and sets. I'm an idiot! And that only 3 years out of university :-(
batterseapower 15y ago

radarsat1 15y ago

Very nice, haven't heard of this before. I think an ideal target for a dependently typed language is scientific array programming, so that you can ensure the sizes of your matrix and array operations check out before performing long-running tasks. If a good array library can be built (e.g. port Haskell's Repa) then it might provide a great foundation for this.

dons 15y ago
With type level naturals recently added to GHC, statically checked arrays are already implementable in Haskell. * http://hackage.haskell.org/package/vector-static http://hackage.haskell.org/package/vector-static * http://hackage.haskell.org/package/hmatrix-static http://hackage.haskell.org/package/hmatrix-static A nice next step would be to optimize out additional runtime bounds checks.
- radarsat1 15y ago
  Very nice! I really look forward to using something like that.

amatus 15y ago

Am I correct in my understanding of these types? Vect a n = vector of a with known length n (n ** Vect a n) = vector of a with unknown length n When I think of it this way it's obvious why filter takes a Vect and returns a pair. Though it seems ugly to have to write each vector function to take both "static" and "dynamic" vectors.

edwinb 15y ago
That's right. You don't normally need to write each vector function both ways. If you can statically know the length (which you normally do in practice, at least in my experience) then you can write down a more precise type. filter serves as an example of what you might do when you need to compute an index dynamically.