Notes on Idris (2017)

https://thebreakfastpost.com/2017/12/02/notes-on-idris/

by jxub • 8 years ago

163 63 8 years ago

a simple program took 25 seconds or more to build

This is surprising, I haven't had that experience, although I've been using the JavaScript backend instead, maybe it's much faster? It takes a few seconds, but not that much, and I'm on mere X220.

Like the author, I also struggle to write clean code in it. I've been writing a personal project to learn functional programming, Idris, Lambda and DynamoDB, and it's been going slowly. Reading the book, and embracing the suggested development method (type, define, refine) has been helpful, and I'm enjoying the whole process, despite a couple of snags with the JS interface.

iainmerrick2• 8 years ago

I was nodding along until I hit that point too. 25 seconds for a simple program??!? That would be a complete dealbreaker.

fiddlerwoaroof4• 8 years ago

It’s not as bad as it sounds because you don’t have to compile your program while you write it. Rather, you send the program to a repl and the type checker tells you about problems. You can even run the total parts pretty quickly in the repl.

The only issue is that the language server seems to have a memory leak or something that leads to it taking a huge amount of memory and getting sluggish over the course of an extended development session.

star-castle2• 8 years ago

2015 MacBook Pro, compiling his 'first cut at it' example:

    # time idris -o Foo Foo.idr
    
    real	0m31.683s
    user	0m30.646s
    sys	0m0.876s

alexashka2• 8 years ago

I've also bought and worked through the book. It's excellent.

My conclusion was that Idris is an academic language (lack of libraries), followed by realizing that the parts of Idris that I like, are almost all covered by Haskell extensions.

For me, Idris is a great peek into what Haskell should/could be, if extensions were better documented and the synergy between them, explained to mere mortals.

pjmlp2• 8 years ago

For me it was also very interesting read, and I also reached a similar conclusion.

Such language features are still too complex for the regular kind of software development many of us do, as the whole team has to fully grasp it.

moosefish• 8 years ago

Any thoughts on Agda? I've always thought that since it's embedded in Haskell, even though it's less 'practical' than Idris it would benefit from the extensive libraries that Haskell brings to the table.

Zalastax• 8 years ago

Usually, Agda programs would not use Haskell libraries very much, even though they could. The reason seems to be that it is an unstable language and we are still figuring out how to do dependent types correctly. To me, working in Agda is like working in a very powerful version of Haskell, but for most people it's more about working in a research language. Idris and Agda are quite similar: don't build a company on them, but expect really cool ideas to spawn from them. Dependent types is really an awesome idea.

fiddlerwoaroof4• 8 years ago

I’ve often thought Idris would be useful for expressing the core business logic of your program, and the you’d use the Haskell or JS backend to do the user-facing parts.

KirinDave2• 8 years ago

I've got a few network services working with Idris and they run okay. The compilation time grows so quickly you can't use it for very large projects though.

Honestly, Haskell dependent-typing is SO MUCH MORE COMPLEX than Idris's "well what if I just write a function that takes a type?" approach, it's not even funny. Even the author of singleton says it's a rough landscape.

Haskell's going to get much closer with QuantifiedConstraints in ghc 8.6, in that it'll simplify a lot of this work, but it's still years out from the simplicity and library unification.

matt-noonan3• 8 years ago

Can you elaborate on the DT / QuantifiedConstraints connection a bit? I haven't thought enough yet about QuantifiedConstraints to see the everyday benefits, but I'm getting contact-excited by everybody else's anticipation of it. I'd love to get some concrete benefits to hold in mind.

ainar-g• 8 years ago

Recently I talked with my cousin, who is also a software engineer, about dependent types, contract programming, invariants, and all that. Among other things I've told him about "type-safe printf" that you can write in Idris. He then asked me, why are there only purely functional languages with this feature. I had no actual answer.

So, does anybody know, why there still isn't a "C/Go/Java with dependent types"? There is support for runtime checking via invariants in e.g. D, but no pre-compile-time checker.

Another question, is there (probably commercial) software that allows you to augment your code with invariant annotations and then check them as a pre-compilation step?

mindB• 8 years ago

I'm not super familiar with it, but ATS[1] might fit the bill in having dependent types and linear types but supporting both functional and imperative paradigms. It's pretty darn obscure, though.

[1] http://www.ats-lang.org/

PeCaN• 8 years ago

ATS is an amazing language, but suffers from being mainly a one-person effort.

doublec's ATS articles are probably the most accessible introduction: https://bluishcoder.co.nz/tags/ats/index.html

Other than that the documentation is very decent for a one-man research project. (I say "research project", and it is, but it has huge practical value as well.)

Still, I have very high hopes for ATS.

star-castle2• 8 years ago

OCaml has a type-safe printf and isn't purely functional.

ATS is essentially 'C with dependent types'. And optionally some other languages with dependent types. You can think of its dependent type checking and theorem-proving as 'pre-compilation', since there's no runtime overhead to it (and since you can separate it out into its own compilation step, including swapping out alternative solvers). ATS's relationship with C is good enough that you can take an arbitrary C program and start tightening its screws by injecting a bit of ATS into it.

lomnakkus• 8 years ago

OCaml has a type-safe printf and isn't purely functional.

Isn't that a non-extensible built-in that's handled "magically" by the compiler? (Apologies if that's wrong, it's been a few years since I've used O'Caml.)

In Idris it's possible to write a type-safe printf entirely in library code -- no magic.

tel• 8 years ago

My understanding is that the research background for a lot of dependently typed designs is based on proof theories where the program/proof represents the theory/constraint one-to-one. Other systems (PRL, Hoare logic) also exist but either have difficulties or haven’t had the same level of research and exploration to reach designs like modern dependently types languages.

So you can easily add imperative steps to such a language, but since you not rely on side-effects for “interesting” behavior, it becomes more difficult to match the underlying proof theories to the kind of verification you’re attempting.

I’m confident people will flood this comment with sources showing how proof theories exist which don’t have these properties, but I think the prevalence of DT langs nowadays does suggest that this particular synthesis is somewhat more productive so far.

alexashka2• 8 years ago

Dependent types are a solution in search of a problem.

Widespread adoption comes from an easy to use, backed by big name, solution to a problem people have been having.

Typescript is a good example - it came with VS Code integration out of the box, and some decent tutorials. It solves the problem of catching dumb type mismatch bugs at compile time, gives jump-to-definition, auto-complete and doesn't cost anything, it's opt-in.

Those are killer usability features!

Dependent types give type theorists a place to try interesting things. That's about it so far.

Regarding invariant annotations - people call those tests :)

nine_k• 8 years ago

Maybe the typical "pedestrian" problems, like lists having non-zero length, or numbers being in a given range, can be checked statically with simpler means that full-on dependent types?

E.g. safe resource deallocaion problem can be seen as a dependent-type problem (only let an initialized resource into a deallocator), but is usually solved with sort-of linear types, or even simpler (though more crude) means.

pron2• 8 years ago

Dependent types are an active area of research. They are one of several different avenues of research into program verification.

The problem is that both their proponents and detractors (as well as those of other verification approaches) confuse research and practice. Think of the field as early stages of pharmaceutical research; experiments in the lab show some promise as well as obstacles, but it's too early to tell which of the approaches, if any, would be able to work at a large scale in field conditions. As long as we don't confuse research and practice we can follow, enjoy and evaluate research on its own terms, rather than judging it based on criteria that may not be relevant at this stage. This is not to say that we cannot point out risks to field adoption, but research is research.

I, too, have my doubts about dependent types, but it's unfair to judge them harshly at this stage, when nobody knows how best to use them.

insulanus• 8 years ago

It's not necessary to be a functional language to have this feature, but in the past it has been the case that mostly functional languages are the ones that do.

The reason I think this happened, is that the language designers of languages like C had things like machine code generation at the top of their mind when writing the language, not abstractions.

Once decisions were made in that mindset, you start making things very difficult to add this without having edge cases.

Anyway, C++ finally has enough features to support this, and the committee will accept it into the standard soon-ish. (Mind you, of course you will still be able to do foolishness like:

std::cout << static_cast<TrustMeImPrintable>(0);

P.S. The feature you need to support this is to be able to pick the types our of the "format sting" (whatever type you use to represent that object), and run a check against the types of the arguments, at compile time.

bakhy• 8 years ago

For C#, and all .NET languages, there are Code Contracts. I've never used them, but they seem to be maintained and relatively easy to use. The docs, with a good example at the end, are here: https://docs.microsoft.com/en-us/dotnet/framework/debug-trac...

Edit: Actually it seems abandoned, with no support for .NET Core right now. Shame.

repolfx• 8 years ago

Imperative and functional programming languages have gone in different directions with respect to proving program correctness. I'm not sure one path is clearly better than another, they're just different.

The imperative world has languages like Dafny or Whiley, where functions are annotated with expressions denoting things that must be true, and the compiler does theorem proving to ensure that the constraints aren't violated. So rather than put things like "length of array A equals length of array B" into types, you put that rule into the code, and the compiler proves that the constraint always holds.

Unfortunately all these languages aren't really mature, whether they use dependent types or contracts. The imperative versions in particular often need you to specify constraints that are obvious.

pron2• 8 years ago

The imperative world has languages like Dafny or Whiley, where functions are annotated with expressions denoting things that must be true, and the compiler does theorem proving to ensure that the constraints aren't violated.

We have that for Java, too: http://www.openjml.org/

The great thing about contracts (as opposed to dependent types) is that they separate specification from verification. You could use proofs (fully- or semi-automatic), but you could also use weaker but cheaper forms of verification, such as concolic tests or randomized tests, generated from the contracts, or, weaker still, runtime assertions. Dependent types tie specification to a specific form of verification (proof).

A standardized specification language like JML can (and does) have many tools offering different forms of verification.

mcguire• 8 years ago

In addition to Dafny (https://github.com/Microsoft/dafny) and Whiley (http://whiley.org/), check out Frama-C (https://frama-c.com/) for C and SPARK (http://www.spark-2014.org/) for Ada.

Both are mature enough to be in use, but are limited primarily by the fact that both languages have manual memory management, which is well understood via separation logic, but poorly supported by the tools.

I've written some blog posts about Frama-C:

* https://maniagnosis.crsr.net/2017/06/AFL-brute-force-search....

* https://maniagnosis.crsr.net/2017/06/AFL-bug-in-quicksearch....

* https://maniagnosis.crsr.net/2017/07/AFL-correctness-of-quic...

* https://maniagnosis.crsr.net/2017/08/AFL-verifying-quicksort...

FeepingCreature2• 8 years ago

D has something like type-safe printf. You can pass the printf string as a compiletime parameter, so ie. format!`%s is bigger than %s`(2, 3, 4) will error during compilation.

ben-schaaf• 8 years ago

It also has similar type safety for native to `byte[]` conversion, ie. `bigEndianToNative!int` takes a `byte[4]`, which you can pass in from a `byte[]` using `data[0..4]`.

icebraining2• 8 years ago

The question is whether that's a special case of the compiler or if it can be implemented by regular D code.

weavie2• 8 years ago

I'm not sure how it would be possible to have dependent types in a non-pure language. A function such as

    append: Vect n elem -> Vect m elem -> Vect (n + m) elem

only works because the compiler can know exactly what is going to happen to those parameters in the function. It can guarantee that there are no side effects that can randomly and non-deterministically come along and change the result. The `Vect n elem` input parameter is always going to be a parameter of n elements. If the function changed n to be (n + 1) then should the result be `Vect (n + 1 + m) elem` or still `Vect (n + m)`? Things get a lot harder to lock down!

ihm2• 8 years ago

+1. If the language is not pure it's unclear how type checking would work. To make things even clearer, consider the following example (in a hypothetical dependently typed language with mutable references):

   f : () -> Type
   f =
     let r = ref 0 in
     fun () ->
       let t = if !r = 0 then Int else String in
       r := r + 1;
       r

   x : f ()
   x = 17

   y : f ()
   y = "foo"

Should this program type check? I think there is a consistent way to talk about type checking here (if there is a canonical ordering of all definitions across all files) but it seems unlikely you'll get a system that's easy to understand.

saurik3• 8 years ago

I don't understand the issue... it is trivial and in fact extremely common-place in impure languages to fundamentally disallow modifications to something's type. C++, which is definitely not pure but yet essentially has dependent types, is easily able to express this exact thought without problem, as your ability to modify things at runtime is extremely limited.

(Of course, the place where C++ is limited is its inability to template over non-concrete values, but I see nothing about its model that fundamentally limits its ability to conceptualize such a thing. It is still technically a dependently typed language even without the ability to do this, of course.) [edit: matt-noonan has told me that I am wrong on that last comment :(... so not "of course".]

    #include <stdlib.h>
    
    template <size_t S, typename E>
    class Vect {
      private:
        E data[S];
    
      public:
        const size_t size() const {
            return S;
        }
    
        E &operator [](size_t i) {
            return data[i];
        }
    
        const E &operator [](size_t i) const {
            return data[i];
        }
    };
    
    template <size_t N, size_t M, typename E>
    Vect<N + M, E> append(const Vect<N, E> &l, const Vect<M, E> &r) {
        Vect<N + M, E> v;
        for (size_t i(0); i != N; ++i)
            v[i] = l[i];
        for (size_t i(0); i != M; ++i)
            v[N+i] = r[i];
        return v;
    }

    int main() {
        Vect<4, int> a;
        Vect<2, int> b;
        Vect<6, int> c = append(a, b);
        Vect<8, int> d = append(a, b);
        return 0;
    }

    test.cpp:36:18: error: no viable conversion from 'Vect<4UL + 2UL aka 6, [...]>' to 'Vect<8, [...]>'
        Vect<8, int> d = append(a, b);
                     ^   ~~~~~~~~~~~~
    test.cpp:4:7: note: candidate constructor (the implicit copy constructor) not viable: no known conversion from 'Vect<4UL + 2UL, int>' to
          'const Vect<8, int> &' for 1st argument
    class Vect {
          ^
    1 error generated.

hota_mazi• 8 years ago

In a nutshell, all dependent type systems are very impractical to use and are widely seen as going way past the point of diminishing returns for real world scenarios. It's not really a coincidence that most illustrations of dependently type programs never go beyond a simple list/stack/vector structure.

I'll take a statically typed language with a decent type system and and assortment of tests any day over a dependently typed language.

dorfsmay• 8 years ago

Is ATS purely functional? Wikipedia lists it as multi-paradigm.

https://en.wikipedia.org/wiki/ATS_(programming_language)

KirinDave2• 8 years ago

Haskell is an excellent imperative language and can simulate some aspects of dependent typing. There are also refinement types which are related.

Typesafe printf is actually a very old trick, typed scheme and even Common Lisp have been showing off macro-based variants for some time.

As for why there aren't more languages directly LIKE Idris and Agda? Probably because the technology and theory to actually make them feasible has existed for less than a full decade. Sorta like how people don't realize sort is an O(n) operation, CRDTs exist, or that we can write lazy succinct parsers of complex tree structures, or can write universal query-insensitive indicies over relational data.

nickpsecurity• 8 years ago

Liquid Haskell is probably the closest to Idris in its goals:

https://wiki.haskell.org/Liquid_Haskell

saurik3• 8 years ago

Technically (and truly), C++ has dependent types, as types can depend on values [edit: matt-noonan has corrected me and pointed out this is wrong, but I think most of this comment is still useful]. (I can't say much about D, but I would believe it does as well; I could also see them having "simplified" away a really critical piece, though.)

A prototypical concept you would expect to find in a dependently typed language is "the ability to have a function that concatenates to arrays of sizes X and Y and returns an array of size X+Y that can be safely verified against further functions that also require arrays given as arguments to have specific lengths".

C++ is a bit indirect in its semantics here, but you will note that most other languages with generic types cannot express this thought (using either real integers or simulating them with types, either of which can be done in C++).

One could easily imagine "filling out" C++ to allow compile time type argument manipulation of more value types without even stressing its model, and in fact that is exactly the direction the language has been going in with constexpr. Here is an article on how to build a compile-time printf using C++14.

http://blogs.microsoft.co.il/sasha/2015/01/29/compile-time-r...

The only real limitation in C++ is that these values have to be relatively "concrete": at some level there has to be a number that can be calculated, as you can only deal with values as you don't have the amazing ability to do unification of program fragments like you have access to in Idris (like, you'd like to be able to say "the length of this array is the same as the length of this runtime string", and then after a bunch of array manipulation claim that you return a string five characters longer than the input string). Again, though: this could be added to C++ without breaking its underlying model. And it definitely is not required by the concept of "dependent types" [edit: matt-noonan points out it is, in fact, required for a language to have "dependent types" :(.]

matt-noonan3• 8 years ago

You can make C++ types that depend on constant values computed at compile-time, but this isn't the same as dependent types. In a hypothetical dependently-typed C++, I would be able to do this:

    template <typename T, int N> struct vec { T data[N]; };
    vec<T,n> repeat(int n, T const& x) {...}

Note the run-time value n appearing in the return type of `repeat`. Because of this, repeat (if we could write it) has a dependent product type: the actual return type varies based on an argument's value.

pjmlp2• 8 years ago

Which is why after so many years of playing with FP on the sidelines, I have come to realize C++ has become a good way to use those concepts, while keeping my CV relevant for the kind of work I do.

Sometimes it feels like a kludge, but then I get to enjoy the nice IDEs, libraries that it has.

If only C++ had proper pattern matching support.

Of course, it isn't the only language I play with.

Yuuri• 8 years ago

Also, in C++ template value parameters are strongly limited to integral types, whereas in dependent types you can use any.

kqr4• 8 years ago

Slightly unrelated but if all you do is stick around in do notation, you will not see why Haskell is the greatest imperative language. That starts happening once you break out of the traditional notation.

cannam3• 8 years ago

Can you expand on that?

kqr4• 8 years ago

I wish I could. Honestly! It's just that while I have experienced it firsthand, I have not spent enough time thinking about it and tinkering with it to be able to succinctly and accurately put into words what it is about.

Some loose thoughts that may or may not make sense:

- In Haskell, effectful computations (such as prints, variable updates, and so on) are first-class values (like integers, strings, and so on). This is the big idea.

- When effectful computations are first-class values, you can store them in data structures like lists. You can associate them with keys in maps. You can even stick them in priority queues.

- When effectful computations are first-class values, you can pass them around as arguments, or send them off as return values.

- When effectful computations are first-class values, you can transform their results, you can chain them together and you can create branches in them.

- When effectful computations are first-class values, you can perform them, then perform then again, then perform them 12 times, then discard them. Or discard them first and never perform them.

- When effectful computations are first-class values, you have decoupled "describing the action" from "executing the action". You can handle the effectful computation without being afraid of performing the effect.

- When description is decoupled from execution, you can abstract over the flow of control. You can have a loop that doesn't always increment its counter, because the incrementing operation is specified in a list somewhere instead.

- Abstracting over the flow of control can be about as confusing as it is dynamic and powerful. It can also be the most clear and obvious solution to some problems.

- Effectful computations as first-class values is a little like functions as first-class values: when you have tried it, you've found it's so convenient that you'd like to have it everywhere. (It's also a little like first-class functions in the sense that you can emulate first-class effects with first-class functions, but it easily becomes unwieldy.)

- Effectful computations as first-class values is even a little like Lisp metaprogramming. In Lisp, the flow of control can be rewired dynamically, because the code itself is a Lisp data structure. In Haskell, the flow of control can be rewired dynamically, because statements don't have to be executed the second you see them.

- The do notation, when used the traditional way, pulls a curtain over how effectful computations are first-class values. Computations in do notation are (to a first approximation) executed as soon as they are seen, because do notation was designed to intentionally hide the ways in which Haskell is a more powerful imperative language.

Sorry if that made things even more confusing than it cleared up.

----

Here's the most basic concrete example I can think of:

    repeated = do {
        putStrLn "Hello";
        putStrLn "Hello";
    }

Huh, the same action is performed two times. I guess I should put it in a variable.

    somewhatDRY = do {
        let greet = putStrLn "Hello";  -- not executed when put into variable
        greet;                         -- executed once here
        greet;                         -- and again here
    }

Oh, the user wanted to specify how many greetings to print.

    countGreetings number = do {
        let greetings =                     -- infinite list of prints,
                repeat (putStrLn "Hello");  -- none of which is executed
        let enough =                        -- we take the first few prints,
                take number greetings;      -- still without executing any
        sequenceA_ enough;                  -- now we execute just the first ones
    }

Huh, I guess I don't even need the do notation anymore.

    countGreetings number =
        let
            greetings = repeat (putStrLn "Hello")
            enough = take number greetings
        in
            sequenceA_ enough

----

In these examples I used sequenceA_, which is a plain library function that takes a list of effectful computations and returns a single effectful computation. The effect of the returned computation is the same as if all the effectful computations in the list was called one after the other.

I mention it's a plain library function because you wouldn't be able to define such a function – not even in the standard library – if effectful computations weren't first-class values...

----

I wrote a comment in the example saying "now we execute just the first ones". That's a lie, actually. Because like any effectful computation, also the return value of countGreetings is a first-class value. Meaning we could assign the return value of countGreetings to a variable, or stick it in a list, and so on, and nothing would be executed.

In order to avoid uncomfortable déjà vu, I'll In order to avoid uncomfortable déjà vu, I'll just leave off here and conclude that when effectful computations are first-class values, there is, in a sense, two phases when the code is run. First there's an evaluation phase, where effectful computations are constructed and passed around. Then there's an execution phase, which actually executes these effects. If your effectful computation isn't hit by the execution phase, it will never be executed – no matter how many times the evaluation phase goes over it.

hderms• 8 years ago

am I understanding that you are suggesting code that explicitly avoids 'do' notation in Haskell can be more imperative than code using 'do' notation? I don't get it

kqr4• 8 years ago

Not more imperative. Just still imperative, but now using features Haskell users wish were available in other imperative languages.

Notes on Idris (2017)

Related Stories