Quicksort in Idris | Hacker News Reader

Quicksort in Idris

github.com

90 pointsmpweiher25 comments

I have some experience with Haskell [1], but I'm absolutely lost here. Can someone explain all this dependent-type syntax that's going on there, or would that be out of scope for a single comment?

[1] The biggest Haskell program I wrote until now was a spellchecker as the final project for a university course.

At a very high level which you may have already found obvious, the type signature for the function basically says "this will take a list, and return a list that is sorted according to these rules, and is a permutation of the original list"

basically proving that quicksort is correct at compile time.

: is used for type annotations instead of :: like in Haskell.

The double asterisk is syntactic sugar for a "dependent pair" http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html... Basically, it is a pair in which the type of the second element depends on the value of the first element.

Here it is being used to pack the result list with a proof that the list satisfies the required properties. The type of the proof must refer to the list, hence the need for dependent types.

The stuff within braces {} are implicit arguments http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html... that are not given explicitly, but are inferred from the type of other arguments.

Type is commonly referred as the kind * in Haskell, the kind of types that have values.

Unlike in vanilla Haskell, the types of data constructors are explicitly stated http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html... In Haskell the "types" of data constructors are kinds, and you need to enable the XKindSignatures extension to give them explicitly. https://downloads.haskell.org/~ghc/latest/docs/html/users_gu...

I'll talk about this declaration only:

    data PreOrder : (a : Type) -> (a -> a -> Type) -> Type where
      PrO : {lte : a -> a -> Type} -- <=
          -> ((x : a) -> (y : a) -> (z : a) -> lte x y -> lte y z -> lte x z) 
             -- transitivity
          -> PreOrder a lte

This declares a function `PreOrder`, which when given some type called `a`, and some function from two `a`s to some other type, produces a type itself. The reason why we see `(a : Type)` to give a name to `a` is that the name is re-used in the second argument.

To produce a value, a constructor is defined `PrO`, with one _implicit_ argument `lte` of type `a -> a -> Type` (note that this `a` is not the same `a` in the type for `PreOrder`!) that can be inferred from the other arguments, and one other argument of a complex type we'll dig into in a moment. If you supply `PrO` with these two things, you will get back an inhabitant of type `PreOrder a lte` - the type that `PreOrder` promises to return when given two things. This is the same as `Maybe` in Haskell being a type-level function, and `Maybe Int` being a type, where `Just` is a constructor that can produce a `Maybe Int` given an `Int`, and `Nothing` is a constructor that can also produce a `Maybe Int` out of nowhere.

    ((x : a) -> (y : a) -> (z : a) -> lte x y -> lte y z -> lte x z)

This type is interesting because of the Curry-Howard correspondence, which basically says that types and propositions are the same thing, and expressions and proofs are the same thing. If you can show there exists some value of some type, you have proven the proposition the type represents. If you think about what `foo :: Int -> String` means in Haskell, you could turn it around to say "If there is an Int, then there is a String." Given some "proof" that `Int` is a non-empty type, that is, a value of type `Int`, can you prove that there exists some value of type `String`? Well, of course you can: `foo _ = "const"` is one such proof, as is `foo = show` or `foo x = if x < 10 then "less" else "greater"`.

In Idris, we can express much more interesting types, such that the existence of some expression of that type is non-trivial. The above type signature is best viewed IMO as a predicate:

    ∀x, y, z ∈ a. x ≤ y ∧ y ≤ z ⇒ x ≤ z

Remember that `a ⇒ b ⇒ c` is the same as `a ∧ b ⇒ c`, just curried, the type signature above is saying that given any x, y, z of type a, and some value indicating that `lte x y` is "true", and some value indicating that `lte y z` is "true", it can be shown that `lte x z` is "true" too. That is, a value of that type is a proof that `lte` is transitive.

Given some _user supplied_ proof of transitivity, and the implicit transitive operator, we have an inhabitant of the type `PreOrder a lte`.

This is dependently typed, because the _type_ of `lte x y` depends on the _value_ of `x` and `y`. When we say `lte : a -> a -> Type` we mean that `lte` is a function from two values of type `a` to some other type.

As an example, we could write `badlte : Int -> Int -> Type; badlte _ _ = Int`. This comparison operator simply ignores its arguments and says the Type of all such comparisons is always `Int`, which is the same as saying that all `Int`s are equivalent, because the binary relation is inhabited for every possible pair of `Int`s. We can prove transitivity with the lambda expression `\x,y,z,ltexy,lteyz => 42`, that is, given three values and two proofs that x <= y and y <= z, we can "prove" x <= z because we can show there's an inhabitant for the type of `Int`. We can make a preorder, and a totalorder, and sort using this order (the result is that any permutation of the input list is fine, because everything's equivalent for comparison).

As a more _interesting_ example, consider the definition of `LTE` for the type `Nat`:

    data LTE  : (n, m : Nat) -> Type where
      LTEZero : LTE Z    right
      LTESucc : LTE left right -> LTE (S left) (S right)

This is an inductive type definition that depends on the values given. `Z`, or zero, the base case of a `Nat`, is less than or equal to every other value, so we can use `right` as a placeholder variable. Given the proof that `left <= right`, we can also say that the successor of `left` (`S left`) is less than the successor of `right`. This is a bog standard inductive proof form, transposed to code. `LTE` becomes a function from two `Nat`s to a `Type` - but it's a partial function, or relation, because not every `Nat` pair produces a `Type`. If we want to prove that 2 is less than or equal to 3, that is, `LTE 2 3`, we can construct it inductively: `LTESucc (LTESucc LTEZero)`, that is, given `0 <= 1` we can show `1 <= 2` and from that `2 <= 3`. But there's no way to chain `LTESucc` and `LTEZero` together to wind up with `LTE 3 2`.

This is rather off-topic, but I want to learn Idris or any other purely functional programming language one day to the point where I would be able to read any program, but most programs written in those languages are so terse and abstract, that I constantly find myself lost in them. The fact that most of those languages permit programmers to define custom operators doesn't help.

I really wish someone would create something like https://cdecl.org/ but for programs in Haskell/Idris/etc.

EDIT: On the article itself, I wonder how much time does it take to compile the resulting program?

I'm in the same boat. I'd really love to see something that's a little bit more beginner friendly than Hoogle.

It's honestly why I think avoiding operator overloading in Java/Go etc was a great idea.

Isn't operator overloading something else than the ability to define custom operators?

What people do in practice with operator overloading is turn regular operators into custom operators that do something different. Your ability to customize behavior is not as extreme as being able to make any custom operators that you want. But the tradeoffs are definitely related.

C# supports operator overloading but not custom operators. That means vectors get to use the plus operator for addition, but no Scalaesque ~~/ operators.

C# is not a language that is generally criticized for operator soup like the ones that support custom operators.

Counter-examples:

* C++ uses bitshift operators for IO. The (in?)famous

    std::cout << "hello world" << std::endl;

Which is such an improvement over

    puts("hello world");

* Ruby on Rails components sometimes redefines `=` as a hash merge. E.g. this

    config.action_mailer.default_options = {from: 'no-reply@example.com'}

actually adds `from` to the default options instead of overriding it completely.

C# may not be generally criticized for that. But there are certainly C# code bases that do get so criticized.

strong disagree, looking up what an operator does takes 5 seconds of reading the doc - if it's a notation that you don't already know -, but the benefits when writing the code are immense.

I've updated the program to compile with the latest version of Idris (1.3): https://gist.github.com/clayrat/ad916323a4e672c1d7dfa3a0ecf1... The compilation takes ~4 sec for me.

Idris is pretty well documented. It feels pretty inaccessible when you're just looking at the code, but in an editor with a plugin (Emacs, Atom, Vim), everything can be inspected, and it feels much more alive that way. Editing dependently-typed code has a particular development style which is very interactive, in which you fill in "holes" (code to be written) with help the from the editor/type-checker, providing feedback and suggestions.

Resources:

http://docs.idris-lang.org/en/latest/tutorial/index.html

https://www.manning.com/books/type-driven-development-with-i...

https://github.com/idris-hackers/software-foundations

https://www.youtube.com/watch?v=4i7KrG1Afbk

The video is a useful start in understanding the Idris experience, but I guess it would be useful to see how much tooling helped in this definition of quick sort?

> I want to learn Idris or any other purely functional programming language one day to the point where I would be able to read any program, but most programs written in those languages are so terse and abstract, that I constantly find myself lost in them.

Elm is purely functional and shares your design sensibilities on this.

It is less terse (by design) than other purely functional languages and (as of the upcoming release) does not support user-defined operators.

I know plenty of folks who got into Elm and then found Haskell and Idris much easier to approach, so it can unlock further learning too!

https://guide.elm-lang.org

Does Elm support dependent types?

Definitely not, but the original commenter was looking for any purely functional programming language, not necessarily one with dependent types. I think we are years away from having an easily comprehensible and usable dependent type system, if it's even possible to have one.

What's interesting is that an algorithm is presented as correct, but which blows up to quadratic behavior given the right input, and since since quicksort uses than tail recursion, could potentially cause a stack overflow. Thus you have a correct, safe algorithm in theory but not in practice.

Which, of course, depends on what you consider to be a "safe" algorithm.

Could you explain about tail-rec causing stack overflow?

Looks like a typo. Quick sort is binary recursive so tail call optimization wouldn’t fix it.

Those are other things you can prove — I actually watched an idris talk where they included the complexity cost in the function and it refuses to run commands over a certain complexity.

Why oh why all the functional programmers I know use sExps. ;)

You didn't guess the right expansion. I meant shortened expressions. Say a function called forallPerm.

There are million better names most of which start by saying what it does. Even foldAllPermutations would be better (if you know what a fold is).

If you're writing in M-expressions do it consistently. If it is logic proof, it is not functional. There I'd expect some lemma names. In plain English.

The datatype called LTEL takes the cake.

> If it is logic proof, it is not functional.

Logic proofs are functional programs; at least, they are isomorphic to them, by Curry-Howard.

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

Reply on news.ycombinator.com