Here's a couple of talks about Idris:

Edwin Brady at London Haskell: https://www.youtube.com/watch?v=vkIlW797JN8

David Christiansen at Haskell DC: 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/

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

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

Haskell is like SML with enforced purity, a different module/typeclass system, and default laziness. LYAH is the best intro. 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!

Sorry for the problems - I was hotlinking to the awesome 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!

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.

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

    > This page abuses rawgit.com. You should complain to its
    > owner.

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.

Edit: Weird, after a couple refreshes it worked, but then I refreshed again and the console disappeared again.

What do you mean by 'systems programming language'?

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.

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.

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

If I paraphrase what you said about Haskell it's true for ATS too:

    "but one of the lovely things about ATS is that despite its reputation as a difficult language, once certain key concepts are tackled, it's relatively easy to program rapidly and create real world products (with a considerably higher assurance of correctness than most languages provide)."

http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.h...

The issue is that is the default mode I would like to work in. Rust is designed to make that the natural mode of working, rather than the exception. Fast, deterministic operations should be easier and more succinct than the managed alternatives – in the context of a systems language that is.

> people assume ATS is more difficult than it is is because much of the documentation and examples for it use a verbose style and heavy proofs.

Then they need better docs. And a better website! And better marketing!

ATS2 has no GC as the default mode of working too. The only reason it is more verbose is because you need the call to free. ATS strives to be explicit in what it does so it's easier to read the code and know what is happening.

Languages with destructors or implicit function calls seem to lean towards the C++ downside of "What does this code really do" when looking at it. I dislike hidden code where there is no easily identifiable call to tell you something is happening.

It's not all roses and unicorns with ATS either of course. What I really want is the next generation of dependently typed system languages which has learnt from the current ones.

So how does ATS enforce memory safety? With Rust you have a bunch of library types that you can reuse that abstract away from the memory management for you. The types make sure you don't screw up. Unfortunately you can't prove things about the `unsafe` blocks, and have to rely on careful auditing, but that only needs to be done once, and then you have a nice, reusable abstraction. Bookkeeping sucks.

> What I really want is the next generation of dependently typed system languages which has learnt from the current ones.

Agreed. At the moment Rust suits me the best, but I definitely don't think it is the end of the road.

Linear types. Much like unique pointers in Rust, the type system tells you when you fail to consume a linear type. A 'free' call would do this. Same with closing files, etc - you use linear types to track that the resource is consumed.

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

1. http://www.idris-lang.org/example/

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

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

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.

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.

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

Algebraic Data Types are types formed from "products and sums" or, in more normal usage, unions and variants. For instance, Booleans are a basic sum ADT:

    data Boolean = True | False

    data Point = Point Double Double Double

    True  : Boolean
    False : Boolean
    Point : Double -> Double -> Double -> Point

    data HTTPHeader = ContentType MimeType
                    | Accept MimeType
                    | Host String
                    ...

    ContentType : MimeType -> HTTPHeader
    Accept      : MimeType -> HTTPHeader
    Host        : String   -> HTTPHeader
    ...

    data Nat = Zero | Succ Nat

    Zero : Nat
    Succ : Nat -> Nat

    Zero
    Succ Zero
    Succ (Succ Zero)
    Succ (Succ (Succ Zero))
    Succ (Succ (Succ (Succ Zero)))
    ...

In particular, we can write a recursive function

    num : Nat -> Int
    num Zero     = 0
    num (Succ n) = 1 + num n

(This duality is actually really key and goes by the name of "Gentzen's Inversion Principle", not that that really matters.)

The final question, about why Maybe is a definition of the option type, should look a little more clear by this point. That said, it betrays a simplification I've used thus far in that <Name> might not be a simple name, but instead a parameterized one where these parameters now occur in the ADT as well. To see if that makes a little sense, try replacing the lowercase parameter names with other concrete types like `Nat` and `Boolean`.

1. "or, in more normal usage, unions and variants". A union is not a product type, it's an unsafe sort of sum type. (The safe sort is sometimes called a "tagged union".) And while "variant" means exactly what you want it to, it's a Microsoft-ism that not everyone will be familiar with.

So: in C-speak, product and sum types are structs and (tagged) unions. In Microsoft-speak, product and sum types are structures and variants.

2. "and 3D points a standard union ADT": again, it's not a union but a struct.

A few other remarks that may help people unfamiliar with this sort of syntax make sense of what you wrote:

3. That notation "Double -> Double -> Double -> Point" can be read as "a function taking a Double, and another Double, and another Double, and returning a Point". The weird notation is because actually it parses as Double -> (Double -> (Double -> Point)), and means it's a function taking a Double and returning a function taking a Double and returning a function taking a Double and returning a Point! The word to look up if that doesn't make sense but you'd like it to is "currying".

4. Relatedly, there is no distinction between a value of type T and a function of no arguments returning type T. That's why tel wrote "Zero : Nat" without any arrow anywhere on the right-hand side. You can (and maybe should) think of this as a function from (nothing) to Nat.

5. (This is implicit in what tel wrote but may be a stumbling block for the newcomer.) When you see something like "data Point = Point Double Double Double" it may not be obvious that the four things on the right-hand side are not at all on an equal footing. The first one (Point) is the name of a constructor. The others (Double Double Double) are the types of its arguments.

On the other hand, product and sum (coproduct) are very well-defined terms which exist far outside any particular language. There's still haziness around choice of category (and, in particular, call-by-value versus call-by-name) but they're an order of magnitude more well-defined. I'd love it if the ADT concept became more widespread and could be easily used as a (low-level) description of more sophisticated typing like struct/variant.

To my ear "union" and "struct" are heavily overloaded since there was never a strict definition of what they should be. Product and Sum (Coproduct) are very well-defined (although, in practice, choice of category leads to some actual haziness especially around CBV/CBN).

In any case, I really appreciate the added detail about how better to use those terms and I'd love if the ideas of sums and products caught on and became a more stable point of communication.

IMHO, A language more suitable for introducing functional programming may be Clojure, F#, Scala, or just 'plain' Haskell.

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.

Idris doesn't need to support (non-dependent) functions or parametric polymorphism, since they're just special-cases of dependent functions. Likewise, typeclasses are just special-cases of dependent records.

When we consider Haskell extensions, many of them are designed to introduce dependently-typed idioms (eg. DataKinds). This makes Idris automatically simpler, since it supports those idioms directly and doesn't have to offer all of the non-dependent parts of Haskell.

On the other hand, typical Haskell programs may use types in a simpler way than typical Idris programs, but that's a separate point. We can focus on simple programs while learning.

Idris has a quantifier which is called Pi in type theory, and this is not the same as Forall (the quantifier present in Haskell and ML). Forall gives you guarantees about uniform behavior over the domain of quantification (this is parametricity), whereas Pi does not.

Idris does however recover parametricity anyway for types, since it lacks an eliminator for the universe (i.e. it doesn't have type-case). But it doesn't have parametric polymorphism for values.

While Idris may be able to eliminate some of the typing constructs in Haskell, I don't think one can say it would be easier to program in than Haskell. The chain of having to assert proofs to the compiler is an extra burden (i.e. refl).

Also, saying that a Pure FP language (Idris) is easier than a non-pure language (Scala), for someone without extensive FP backround, is an interesting comment. Part of the intimidation of Haskell is it's purity, and this extends to Idris.

(Moreover, I did also include SML in my list of languages better for beginners than Haskell and Scala incidentally. If the purity is the problem, then SML is a great place to start. Begin with proving by induction that an SML program is pure or impure—this will motivate having it internalized in the type theory.)

Moreover, you don't even need to use the "proving" parts of Idris. You can use the fragment of Idris which is a fixed Haskell, and move on up to the more interesting bits when they become useful to you. For instance, you can write partial programs (and coprograms) in Idris without doing any proofs; then at the end, you can have someone help you shore it up with proofs that it is sound.

    typedef positive_int: int {
        ensure {this > 0}
    }
    typedef ambulance: vehicle {
        ensure {this.has_siren && this.has_bed && this.color == "red"}
    }

(aside: The other main problem I have with functional languages is the following, I'm not sure what to call it but it bites me every time: You finally find out how to do what you want in an elegant functional way, you code it up and you're happy. Then, you want to make a small modification, but it turns out that it's impossible with the current code, and you have to rewrite everything with much less abstraction. I can't remember a great example from the top of my head, but a simple one is, you'd like to add a progress bar to a computation. It's trivial in imperative languages, but much harder in functional style.)

Well, right now some languages are able to verify that a variable is non-null at compile time (C#). It should be possible to add range requirements to numeric types (e.g. i > 5), and (non-)equality requirements for most types. Intersections and unions of these requirements is trivial, so the compiler could work out possibly allowed and disallowed value (ranges). If we only allow these simple constraints, it is essentially constraint-solving at compile time. The compiler can "understand" these simple types, and it can see that a positive int (or a non-null Vehicle) is required, and propagate that backwards and see whether it is violated.

(One could go a bit further and add almost arbitrary expressions (of C++11 constexpr strength). If the compiler can't convert the expression to a union or intersection of things it understands, it can still check if a given constant violates the condition. E.g. it is known that x=5, and the precondition of a function is x2 != 25, then this is a violation. I don't know how useful this would be, though. One could also add "lemmas" to aid the compiler, e.g. "I guarantee that x > 10 in this branch".)

For instance:

    -- exporting only the type Positive, the extractor `getInt`, and the 
    -- smart constructor `pint` ensures constraint safety.
    module Positive (Positive (getInt), pint) where

      newtype Positive = Positive { getInt :: Int }

      -- creation of Positive types ensures that constraint
      pint :: Int -> Maybe Positive
      pint i | i > 0     = Just i
             | otherwise = Nothing

A similar method can be done with the ambulance type, though I don't think modeling the world like that in functional types is a good design.

That's exactly what I'm asking for :-). It should be possible to create restricted types that are checked at runtime. For example, the fabs function would return a float which is guaranteed to be >= 0. The sqrt function would require the argument to be positive.

    float x;
    ...         // arbitrary code
    sqrt(x);    // warning, possible invalid argument

    float y;
    y = fabs(...);  // y is now float<positive>
    sqrt(x);    // no warning

    float z;
    z = -1.0;
    sqrt(z);    // error: invalid argument, argument z of type float
                // fails constraint z > 0. z is constant -1.0

This may sound crazy, but I think the parts are already out there. C#'s non-nullable types are a very weak version of this (the compiler can infer if something could possibly be null, and complains if you assign it to a non-nullable type). Many compilers also track uninitialized variables, and only let you assign to them, not from them. They are also effectively a restricted version of the original type (every time you declare a float argument, you actually mean float<initialized>).

Another ingredient is control-flow analysis. For example there is the excellent PySonar [1] that performs a whole-program analysis of Python programs and is able to infer types (including union types where it is not sure). In Python, values and types are somewhat blurred IMHO. Instead of variables, Python actually has `names`, and each name has a `type` and a `value` inside. Inferring what `type` a `name` could have is a bit like inferring what value a variable could have in other languages. So I think some of the lessons learned there could be valuable for building a something like this, too.

[1] http://yinwang0.wordpress.com/2010/09/12/pysonar/

Indeed, everything you've written can be fairly trivially implemented in Haskell, though inference and annotation would feel different. The real challenge comes in when you've got an arbitrary "test" expression which must be satisfied by the statics of your language.

For instance, your original example had ensure blocks

    ensure { x.left > 10 && x.right < 30 }

Which is exactly the path taken by "DT" languages like Agda, Coq, Idris, ATS. The upshot is that you get arbitrarily powerful static queries. The downside is that your type system is exactly as complex as your language itself and you have to shuffle around proofs of various invariants being held because it's an NP-complete search problem for the compiler to find them for itself.

I highly recommend trying out Coq if this kind of stuff interests you. I recommend Coq over Agda/Idris because you're going to be learning new syntax anyway and Coq has better literature out there:

    http://www.cis.upenn.edu/~bcpierce/sf/
    http://adam.chlipala.net/cpdt/

The thing that bothers me about implementing these constraints the Haskell or Idris way (or in any other DT language I've encountered) is that it feels a lot like template metaprogramming in C++. Define integers with nested types as Zero and the sequence of successors (data Nat = Z | S Nat) seems a lot like defining integers with the Peano axioms using nested C++ templates - possible, even neat, but a bit crazy. Maybe that feeling goes away when you're more familiar with the languages.

Btw. I've just found out that Spec# (an extension of C#) almost has what I described... you can define preconditions and invariants that are checked at least at runtime, but a static checker tries to proove as much as possible at compile time. Its a pity it is no longer developed, this could have been the static type checked language for the rest of us:

    http://rise4fun.com/specsharp/

http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/

The core idea here is called the Refinement Type which is basically what you're looking for. In order to power this type system Liquid Haskell depends on a full SMT solver, though, which is a rather large hammer to wield.

As it regards to Peano arithmetic in DT languages the Peano naturals data type is awkward for doing math... but FANTASTIC for defining the properties of recursion and induction. Indeed, what you find is that the Peano nats show up everywhere as being a stable foundation for complex proofs and smart recursive functions.

It's a very similar feature to Haskell's lists. Competent Haskell programers do not use lists when they want arrays or vectors—the latter types are naturally far more convenient when in their application space. But lists are not abolished! They're fantastically useful as control structures indicating sequential recursion.

Typically you think of data types as forming their meaning through construction. You use numbers by constructing them according to arithmetic properties. Another way to do it, though, especially with recursive ADTs and inductive families, is to think of a type's meaning as being derived from how you break it down.

The canonical way to break down a list is to find some way of combining the head of the list with the broken-down version of the tail of the list. In Haskell that is called foldr

    --       combiner         zero list   result
    foldr :: (a -> b -> b) -> b -> [a] -> b

    let ls = Cons 1 (Cons 2 (Cons 3 Nil)))
    
    foldr comb zero ls =
             comb 1 (comb 2 (comb 3 zero)))

No need for runtime checks/errors, no need to solve the halting problem, etc.

That depends a lot on how you code your program. You'll havr as much difficulties in imperative style if you didn't think up front about that feature (or any similar ones). What you want is modularity, and it means the ability to separate concerns at the language core. Luckily, un FP, functions being first class, you can easily extract functions out of an algorithm, and the pass them as parameters. So in your example, you'd parameterize on the function which does that computation step, and plug in that very function wrapped with one doing the progress bar update. With a well written codebase, this sort of things are just one refactoring away. This exercise being easier or harder is mostly a question of being used to the language imho.

Of course, you could just pull a Clojure and throw everything into maps.

this causes the console not to load. It would be better to host the js yourself, probably.

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.