Idris function to construct empty `List a` where `a` is bound to an instance of `Ord`?

Question

I've only read the standard tutorial and fumbled around a bit, so I may be missing something simple.

If this isn't possible in Idris, please explain why. Furthermore, if can be done in another language please provide a code sample and explain what's different about that language's type system that makes it possible.

Here's my approach. Problems first arise in the third section.

Create an empty list of a known type

 v : List Nat
 v = []

This compiles and manifests in the REPL as [] : List Nat. Excellent.

Generalize to any provided type

 emptyList : (t : Type) -> List t
 emptyList t = []

 v' : List Nat
 v' = emptyList Nat

Unsurprisingly, this works and v' == v.

Constrain type to instances of Ord class

emptyListOfOrds : Ord t => (t : Type) -> List t
emptyListOfOrds t = []

v'' : List Nat
v'' = emptyListOfOrds Nat     -- !!! typecheck failure

The last line fails with this error:

When elaborating right hand side of v'':
Can't resolve type class Ord t

Nat is an instance of Ord, so what's the problem? I tried replacing the Nats in v'' with Bool (not an instance of Ord), but there was no change in the error.

Another angle...

Does making Ord t an explicit parameter satisfy the type checker? Apparently not, but even if it did requiring the caller to pass redundant information isn't ideal.

 emptyListOfOrds' : Ord t -> (t : Type) -> List t
 emptyListOfOrds' a b = []

 v''' : List Nat
 v''' = emptyListOfOrds (Ord Nat) Nat     -- !!! typecheck failure

The error is more elaborate this time:

 When elaborating right hand side of v''':
 When elaborating an application of function stackoverflow.emptyListOfOrds':
         Can't unify
                 Type
         with
                 Ord t

         Specifically:
                 Can't unify
                         Type
                 with
                         Ord t

I'm probably missing some key insights about how values are checked against type declarations.

Answer 1

As other answers have explained, this is about how and where the variable t is bound. That is, when you write:

emptyListOfOrds : Ord t => (t : Type) -> List t

The elaborator will see that 't' is unbound at the point it is used in Ord t and so bind it implicitly:

emptyListOfOrds : {t : Type} -> Ord t => (t : Type) -> List t

So what you'd really like to say is something a bit like:

emptyListOfOrds : (t : Type) -> Ord t => List t

Which would bind the t before the type class constraint, and therefore it's in scope when Ord t appears. Unfortunately, this syntax isn't supported. I see no reason why this syntax shouldn't be supported but, currently, it isn't.

You can still implement what you want, but it's ugly, I'm afraid:

Since classes are first class, you can give them as ordinary arguments:

emptyListOfOrds : (t : type) -> Ord t -> List t

Then you can use the special syntax %instance to search for the default instance when you call emptyListOfOrds:

v'' = emptyListOfOrds Nat %instance

Of course, you don't really want to do this at every call site, so you can use a default implicit argument to invoke the search procedure for you:

emptyListOfOrds : (t : Type) -> {default %instance x : Ord t} -> List t
v'' = emptyListOfOrds Nat

The default val x : T syntax will fill in the implicit argument x with the default value val if no other value is explicitly given. Giving %instance as the default then is pretty much identical to what happens with class constraints, and actually we could probably change the implementation of the Foo x => syntax to do exactly this... I think the only reason I didn't is that default arguments didn't exist yet when I implemented type classes at first.

Answer 2

You could write

emptyListOfOrds : Ord t => List t
emptyListOfOrds = []

v'' : List Nat
v'' = emptyListOfOrds

Or perhaps if you prefer

 v'' = emptyListOfOrds {t = Nat}

If you ask for the type of emptyListOfOrds the way you had written, you get

Ord t => (t2 : Type) -> List t2

Turing on :set showimplicits in the repl, and then asking again gives

{t : Type} -> Prelude.Classes.Ord t => (t2 : Type) -> Prelude.List.List t2

It seems specifying an Ord t constraint introduces an an implicit param t, and then your explicit param t gets assigned a new name. You can always explicitly supply a value for that implicit param, e.g. emptyListOfOrds {t = Nat} Nat. As far as if this is the "right" behavior or a limitation for some reason, perhaps you could open an issue about this on github? Perhaps there's some conflict with explicit type params and typeclass constraints? Normally typeclasses are for when you have things implicitly resolved... though I think I remember there being syntax for obtaining an explicit reference to a typeclass instance.

Answer 3

Not an answer, just some thoughts.

The problem here is that (t : Type) introduces new scope that extends to the right but Ord t is outside of this scope:

*> :t emptyListOfOrds 
emptyListOfOrds : Ord t => (t2 : Type) -> List t2

You can add class constraint after introducing type variable:

emptyListOfOrds : (t : Type) -> Ord t -> List t
emptyListOfOrds t o = []

But now you need to specify class instance explicitly:

instance [natord] Ord Nat where
  compare x y = compare x y

v'' : List Nat
v'' = emptyListOfOrds Nat @{natord}

Maybe it is somehow possible to make Ord t argument implicit.