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

Question

I read only the standard textbook and rummaged around a bit, so I might be something simple.

If this is not possible in Idris, explain why. In addition, if it can be done in another language, please indicate a code sample and explain what distinguishes this language system, which allows it to be done.

Here is my approach. First, problems arise in the third section.

Create an empty list of known type

v : List Nat v = [] 

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

Summarize any type provided

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

No wonder this works and v' == v .

Type of restriction for instances of class Ord

 emptyListOfOrds : Ord t => (t : Type) -> List t emptyListOfOrds t = [] v'' : List Nat v'' = emptyListOfOrds Nat -- !!! typecheck failure 

The last error of 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 Nat with v'' with Bool (and not with an Ord instance), but there was no error.

Another angle ...

Does make Ord t an explicit type-checking parameter? Apparently not, but even if it required the caller to transmit redundant information, it’s not ideal.

  emptyListOfOrds' : Ord t -> (t : Type) -> List t emptyListOfOrds' ab = [] v''' : List Nat v''' = emptyListOfOrds (Ord Nat) Nat -- !!! typecheck failure 

The error this time is more complicated:

  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 probably miss some key information about how values ​​are checked against type declarations.

Answer 1

As the other answers explained, it is about how and where the variable t is related. That is, when you write:

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

The developer will see that 't' is unconnected at the point at which it is used in Ord t and therefore binds it implicitly:

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

So, what would you like to say, it's something like:

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

To bind t to a class type restriction, and therefore it appears in the region when Ord t appears. Unfortunately, this syntax is not supported. I see no reason why this syntax should not be supported, but currently it is not.

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

Since classes are first-class, you can specify them as regular arguments:

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

Then you can use the special %instance syntax to find the default instance when calling emptyListOfOrds :

 v'' = emptyListOfOrds Nat %instance 

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

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

Syntax default val x : T populate the implicit argument x with the default value val if no other value is explicitly specified. Providing %instance as the default value is pretty much identical to what happens with class constraints, and in fact we could probably change the syntax implementation of Foo x => to do just that ... I think the only reason which I have not been to, is that the default arguments did not exist when I first introduced class classes.

Answer 2

You can write

 emptyListOfOrds : Ord t => List t emptyListOfOrds = [] v'' : List Nat v'' = emptyListOfOrds 

Or perhaps if you prefer

  v'' = emptyListOfOrds {t = Nat} 

If you request the type emptyListOfOrds as you wrote, you get

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

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

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

It seems that specifying the constraint Ord t introduces the implicit parameter t , and then your explicit parameter t given a new name. You can always specify a value for this implicit parameter, for example. emptyListOfOrds {t = Nat} Nat . If for some reason this is the “right” behavior or restriction for some reason, maybe you could open the question about it on github? Perhaps there is a conflict with explicit type parameters and class restrictions? Typically, type types look when you have something implicitly permitted ... although I think I remember that there is a syntax for getting an explicit reference to an instance of typeclass.

Answer 3

Not an answer, just some thoughts.

The problem here is that (t : Type) introduces a new scope that extends to the right, but Ord t goes beyond that scope:

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

You can add a class constraint after entering a variable of type:

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

But now you need to explicitly specify an instance of the class:

 instance [natord] Ord Nat where compare xy = compare xy v'' : List Nat v'' = emptyListOfOrds Nat @{natord} 

Perhaps it is possible to make the argument Ord t implicit.