98 ms·

Try Idris

152 points by jcurbo 13y ago

jcurbo 13y ago
For those curious what Idris is, from http://www.idris-lang.org/ http://www.idris-lang.org/ : "Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type." Here's a couple of talks about Idris: Edwin Brady at London Haskell: https://www.youtube.com/watch?v=vkIlW797JN8 https://www.youtube.com/watch?v=vkIlW797JN8 David Christiansen at Haskell DC: http://bmsherman.github.io/idris-drc-3-26-14/ http://bmsherman.github.io/idris-drc-3-26-14/ And there's a tutorial and other docs available here: http://www.idris-lang.org/documentation/ http://www.idris-lang.org/documentation/
- 14113 13y ago
  Just to note, Edwin was the original author of Idris, so I'd definitely recommend watching his talk. Edit: Given that my comment seems fairly high at the moment, I'll post a link to his PhD thesis, which seems to be the genesis of Idris for anyone interested: http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf
- ryanartecona 13y ago
  I'll add: if all this seems too opaque to jump into at once (and especially if you're unfamiliar with Haskell or other FP languages), don't give up on FP! A "functional" language is not always a "pure" language, and a "pure functional" language certainly does not always have dependent types. These concepts build on each other. A great intro to FP is "Programming in Standard ML". Concise, precise, and very approachable. SML is functional, but not pure nor dependently-typed (though purity is encouraged). http://www.cs.cmu.edu/~rwh/smlbook/book.pdf http://www.cs.cmu.edu/~rwh/smlbook/book.pdf Haskell is like SML with enforced purity, a different module/typeclass system, and default laziness. LYAH is the best intro. http://learnyouahaskell.com/ http://learnyouahaskell.com/ Idris is aimed primarily at those already familiar with Haskell, so don't be discouraged if the online REPL feels too foreign!
deleted 13y ago
[deleted]
Udo 13y ago
> You can use the REPL above to play I don't see anything like that on my screen (OS X, Firefox latest). It's basically just three lines of code without any interaction.
- RussianCow 13y ago
  Same thing here, in both Firefox and Chrome. Edit: Weird, after a couple refreshes it worked, but then I refreshed again and the console disappeared again.
- chrisdevereux 13y ago
  Same for me (OS X, Safari latest)
- fhars 13y ago
  The beginning of the HTML (including the head with the script links) is [sometimes] missing from the page sent by the server.
sabalaba 13y ago
I discovered Idris when I was playing around with Agda last summer. It's cool to see a systems programming language with dependent types.
- Dewie 13y ago
  > It's cool to see a systems programming language with dependent types. What do you mean by 'systems programming language'?
  - Rusky 13y ago
    The tutorial says "The goal of the IDRIS project is to build a dependently typed language suitable for verifiable systems programming. To this end, IDRIS is a compiled language which aims to generate efficient executable code. It also has a lightweight foreign function interface which allows easy interaction with external C libraries." I generally think of systems programming as drivers, kernels, embedded stuff, and performance-sensitive applications like game engines. Not sure how far in this direction IDRIS is going though. It feels a lot like the same niche as OCaml, with dependent types.
    - edwinb 13y ago
      I tend not to use the phrase "systems programming" any more. "General purpose" is probably better (or my current favourite "Pac-man complete"). I should probably edit the tutorial to that effect. We've done simple network protocols and packet formats (I had a student working on DNS for example) but not driver or kernel level things. That said, some people are experimenting with lower level things (thinking about making a minimal run time system with no garbage collection for example). It's not a primary goal, but it'll be interesting to see what comes of it.
      - bjz_ 13y ago
        > I should probably edit the tutorial to that effect. Yes please do. Idris is a lovely language for bringing dependent types closer to the realm of production code, but giving people false hopes is a little cruel :)
fprotthetarball 13y ago
"This website abuses rawgit.com. You should complain to its owner."
- double051 13y ago
  Yeah, saw this alert after switching between 'Console' and 'Compile'.
riffraff 13y ago
> Failed to load resource: the server responded with a status of 503 (Service Temporarily Unavailable) http://rawgit.com/chrisdone/jquery-console/master/jquery.console.js http://rawgit.com/chrisdone/jquery-console/master/jquery.con... this causes the console not to load. It would be better to host the js yourself, probably.
peter_l_downs 13y ago
Here's what I saw: http://i.imgur.com/4yNB6t4.png http://i.imgur.com/4yNB6t4.png > This page abuses rawgit.com. You should complain to its > owner.
- erikano 13y ago
  They can use cdn.rawgit.com instead, which is ok to use in production according to http://rawgit.com/#cdn http://rawgit.com/#cdn
tel 13y ago
Sadly the console seems to be missing and the compiler doesn't emit errors. The second is more sad since so much of the dynamics of programming Idris comes from the trying to get its statics to compile. In particular, you will spend an inordinate amount of time staring down collections of type holes trying to solve the puzzle they present. None of that gets reflected in the compiled Javascript.
orf 13y ago
Functional languages interest me, but are not very approachable. I mean I looked at the examples[1] page for Idris and came away completely confused, why he hell does this sequence of characters "data Nat = Z | S Nat" define a natural number? Or "data Maybe a = Nothing | Just a" somehow defines an option type. It would be good to have an introduction for people not too familiar with functional languages. 1. http://www.idris-lang.org/example/ http://www.idris-lang.org/example/
- gnuvince 13y ago
  It's the traditional, inductive definition of natural numbers. You give a base case (Z = Zero) and an inductive case (S Nat = Successor of Nat). So Z is a natural number, S Z is also a natural number and corresponds to 1, S (S Z) corresponds to 2, etc.
- platz 13y ago
  While not incorrect, I think the "functional language" designation is overly broad. Worst case, I'd hate for people to get turned off of functional languages because of difficulties understanding a relatively-advanced dependently-typed language such as Idris. IMHO, A language more suitable for introducing functional programming may be Clojure, F#, Scala, or just 'plain' Haskell.
  - jonsterling 13y ago
    Clojure has little relevance to functional programming: functions are the smoke, but types are the fire. F# might be a good choice for an introduction though (if you're willing to sacrifice the good parts of ML for the bad parts of .Net). Scala and Haskell both have (in decreasing order) massively more complicated type systems than Idris, so I would certainly not recommend those! Moreover, good Scala and Haskell code tends to be way more difficult to understand initially than good Idris code. YMMV. An introductory language needs to be simple enough that a learner can hold all of it in her/his head. SML and Idris fit that bill, IMO, in a way that Haskell and Scala cannot.
    - 13y ago
pufuwozu 13y ago
Hey everyone, I'm the creator! Sorry for the problems - I was hotlinking to the awesome http://rawgit.com/ http://rawgit.com/ website during development and forgot to remove it before posting it on Twitter. The website should be fixed in just a few seconds. Thanks for trying it out!
skybrian 13y ago
I'm glad to see dependent types move a bit closer to practical programming. I read (well, skimmed) the tutorial and learned a little of what it's all about. Being able to pass around assertions as first-class objects seems pretty interesting. However, I'm still confused about what's happening at compile time versus runtime. Apparently some functions can be used in proofs (and are therefore evaluated at compile time), while some proofs must be evaluated at runtime? The notation isn't very helpful here. Since types are no longer strictly compile time and values are no longer strictly runtime, it seems like we need some other way to easily distinguish compile time and runtime.
- ihm 13y ago
  See this page (https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usage-analysis https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usag...) for info on erasure. Unused proof values or indices in data types used for static checking are erased at compile time via usage analysis (if you don't use it in the RHS of a function definition, it gets erased). If you want to ensure that the indices of your data type or arguments to your function are erased, you can use the new dot notation. E.g., if you give a function called "half" the following type half : (n : Nat) -> .(pf : Even n) -> Nat then the compiler will complain if the proof argument is actually used.
- tel 13y ago
  I may be misinterpreting your statement, but passing around assertion objects is a common feature of many DT languages (Coq, Agda, Idris, Epigram, ATS, etc)
tempodox 13y ago
This is one REPL, and compiler, that does not work and doesn't react to user interaction. That doesn't exactly inspire confidence.

152 points by jcurbo 13y ago

For those curious what Idris is, from http://www.idris-lang.org/ http://www.idris-lang.org/ : "Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type." Here's a couple of talks about Idris: Edwin Brady at London Haskell: https://www.youtube.com/watch?v=vkIlW797JN8 https://www.youtube.com/watch?v=vkIlW797JN8 David Christiansen at Haskell DC: http://bmsherman.github.io/idris-drc-3-26-14/ http://bmsherman.github.io/idris-drc-3-26-14/ And there's a tutorial and other docs available here: http://www.idris-lang.org/documentation/ http://www.idris-lang.org/documentation/

14113 13y ago
Just to note, Edwin was the original author of Idris, so I'd definitely recommend watching his talk. Edit: Given that my comment seems fairly high at the moment, I'll post a link to his PhD thesis, which seems to be the genesis of Idris for anyone interested: http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf
ryanartecona 13y ago
I'll add: if all this seems too opaque to jump into at once (and especially if you're unfamiliar with Haskell or other FP languages), don't give up on FP! A "functional" language is not always a "pure" language, and a "pure functional" language certainly does not always have dependent types. These concepts build on each other. A great intro to FP is "Programming in Standard ML". Concise, precise, and very approachable. SML is functional, but not pure nor dependently-typed (though purity is encouraged). http://www.cs.cmu.edu/~rwh/smlbook/book.pdf http://www.cs.cmu.edu/~rwh/smlbook/book.pdf Haskell is like SML with enforced purity, a different module/typeclass system, and default laziness. LYAH is the best intro. http://learnyouahaskell.com/ http://learnyouahaskell.com/ Idris is aimed primarily at those already familiar with Haskell, so don't be discouraged if the online REPL feels too foreign!

deleted 13y ago

[deleted]

Udo 13y ago

> You can use the REPL above to play I don't see anything like that on my screen (OS X, Firefox latest). It's basically just three lines of code without any interaction.

RussianCow 13y ago
Same thing here, in both Firefox and Chrome. Edit: Weird, after a couple refreshes it worked, but then I refreshed again and the console disappeared again.
chrisdevereux 13y ago
Same for me (OS X, Safari latest)
fhars 13y ago
The beginning of the HTML (including the head with the script links) is [sometimes] missing from the page sent by the server.

sabalaba 13y ago

I discovered Idris when I was playing around with Agda last summer. It's cool to see a systems programming language with dependent types.

Dewie 13y ago
> It's cool to see a systems programming language with dependent types. What do you mean by 'systems programming language'?
- Rusky 13y ago
  The tutorial says "The goal of the IDRIS project is to build a dependently typed language suitable for verifiable systems programming. To this end, IDRIS is a compiled language which aims to generate efficient executable code. It also has a lightweight foreign function interface which allows easy interaction with external C libraries." I generally think of systems programming as drivers, kernels, embedded stuff, and performance-sensitive applications like game engines. Not sure how far in this direction IDRIS is going though. It feels a lot like the same niche as OCaml, with dependent types.
  - edwinb 13y ago
    I tend not to use the phrase "systems programming" any more. "General purpose" is probably better (or my current favourite "Pac-man complete"). I should probably edit the tutorial to that effect. We've done simple network protocols and packet formats (I had a student working on DNS for example) but not driver or kernel level things. That said, some people are experimenting with lower level things (thinking about making a minimal run time system with no garbage collection for example). It's not a primary goal, but it'll be interesting to see what comes of it.
    - bjz_ 13y ago
      > I should probably edit the tutorial to that effect. Yes please do. Idris is a lovely language for bringing dependent types closer to the realm of production code, but giving people false hopes is a little cruel :)

fprotthetarball 13y ago

"This website abuses rawgit.com. You should complain to its owner."

double051 13y ago
Yeah, saw this alert after switching between 'Console' and 'Compile'.

riffraff 13y ago

> Failed to load resource: the server responded with a status of 503 (Service Temporarily Unavailable) http://rawgit.com/chrisdone/jquery-console/master/jquery.console.js http://rawgit.com/chrisdone/jquery-console/master/jquery.con... this causes the console not to load. It would be better to host the js yourself, probably.

peter_l_downs 13y ago

Here's what I saw: http://i.imgur.com/4yNB6t4.png http://i.imgur.com/4yNB6t4.png > This page abuses rawgit.com. You should complain to its > owner.

erikano 13y ago
They can use cdn.rawgit.com instead, which is ok to use in production according to http://rawgit.com/#cdn http://rawgit.com/#cdn

tel 13y ago

Sadly the console seems to be missing and the compiler doesn't emit errors. The second is more sad since so much of the dynamics of programming Idris comes from the trying to get its statics to compile. In particular, you will spend an inordinate amount of time staring down collections of type holes trying to solve the puzzle they present. None of that gets reflected in the compiled Javascript.

orf 13y ago

Functional languages interest me, but are not very approachable. I mean I looked at the examples[1] page for Idris and came away completely confused, why he hell does this sequence of characters "data Nat = Z | S Nat" define a natural number? Or "data Maybe a = Nothing | Just a" somehow defines an option type. It would be good to have an introduction for people not too familiar with functional languages. 1. http://www.idris-lang.org/example/ http://www.idris-lang.org/example/

gnuvince 13y ago
It's the traditional, inductive definition of natural numbers. You give a base case (Z = Zero) and an inductive case (S Nat = Successor of Nat). So Z is a natural number, S Z is also a natural number and corresponds to 1, S (S Z) corresponds to 2, etc.
platz 13y ago
While not incorrect, I think the "functional language" designation is overly broad. Worst case, I'd hate for people to get turned off of functional languages because of difficulties understanding a relatively-advanced dependently-typed language such as Idris. IMHO, A language more suitable for introducing functional programming may be Clojure, F#, Scala, or just 'plain' Haskell.
- jonsterling 13y ago
  Clojure has little relevance to functional programming: functions are the smoke, but types are the fire. F# might be a good choice for an introduction though (if you're willing to sacrifice the good parts of ML for the bad parts of .Net). Scala and Haskell both have (in decreasing order) massively more complicated type systems than Idris, so I would certainly not recommend those! Moreover, good Scala and Haskell code tends to be way more difficult to understand initially than good Idris code. YMMV. An introductory language needs to be simple enough that a learner can hold all of it in her/his head. SML and Idris fit that bill, IMO, in a way that Haskell and Scala cannot.
  - 13y ago

pufuwozu 13y ago

Hey everyone, I'm the creator! Sorry for the problems - I was hotlinking to the awesome http://rawgit.com/ http://rawgit.com/ website during development and forgot to remove it before posting it on Twitter. The website should be fixed in just a few seconds. Thanks for trying it out!

skybrian 13y ago

I'm glad to see dependent types move a bit closer to practical programming. I read (well, skimmed) the tutorial and learned a little of what it's all about. Being able to pass around assertions as first-class objects seems pretty interesting. However, I'm still confused about what's happening at compile time versus runtime. Apparently some functions can be used in proofs (and are therefore evaluated at compile time), while some proofs must be evaluated at runtime? The notation isn't very helpful here. Since types are no longer strictly compile time and values are no longer strictly runtime, it seems like we need some other way to easily distinguish compile time and runtime.

ihm 13y ago
See this page (https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usage-analysis https://github.com/idris-lang/Idris-dev/wiki/Erasure-by-usag...) for info on erasure. Unused proof values or indices in data types used for static checking are erased at compile time via usage analysis (if you don't use it in the RHS of a function definition, it gets erased). If you want to ensure that the indices of your data type or arguments to your function are erased, you can use the new dot notation. E.g., if you give a function called "half" the following type half : (n : Nat) -> .(pf : Even n) -> Nat then the compiler will complain if the proof argument is actually used.
tel 13y ago
I may be misinterpreting your statement, but passing around assertion objects is a common feature of many DT languages (Coq, Agda, Idris, Epigram, ATS, etc)

tempodox 13y ago

This is one REPL, and compiler, that does not work and doesn't react to user interaction. That doesn't exactly inspire confidence.