Automatic detection of domain for dependent type function in Idris

Question

Idris language tutorial has simple and understandable example of the idea of Dependent Types: http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#first-class-types

Here is the code:

isSingleton : Bool -> Type
isSingleton True = Int
isSingleton False = List Int

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

sum : (single : Bool) -> isSingleton single -> Int
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs

I decided to spend more time on this example. What bothers me in sum function is that I need to explicitly pass single : Bool value to function. I don't want to do this and I want compiler to guess what this boolean value should be. Hence I pass only Int or List Int to sum function there should be 1-to-1 correspondence between boolean value and type of argument (if I pass some other type this just mustn't type check).

Of course, I understand, this is not possible in general case. Such compiler tricks require my function isSingleton (or any other similar function) be injective. But for this case it should be possible as it seems to me...

So I started with next implementation: I just made single argument implicit.

sum : {single : Bool} -> isSingleton single -> Int
sum {single = True} x = x
sum {single = False} [] = 0
sum {single = False} (x :: xs) = x + sum' {single = False} xs

Well, it doesn't really solve my problem because I still need to call this function in the next way:

sum {single=True} 1

But I read in tutorial about auto keyword. Though I don't quite understand what auto does (because I didn't find description of it) I decided to patch my function just a little bit more:

sum' : {auto single : Bool} -> isSingleton single -> Int
sum' {single = True} x = x
sum' {single = False} [] = 0
sum' {single = False} (x :: xs) = x + sum' {single = False} xs

And it works for lists!

*DepFun> :t sum'
sum' : {auto single : Bool} -> isSingleton single -> Int
*DepFun> sum' [1,2,3]
6 : Int

But doesn't work for single value :(

*DepFun> sum' 3
When checking an application of function Main.sum':
        List Int is not a numeric type

Can someone explain is it actually possible to achieve my goal in such injective function usages currently? I watched this short video about proving something is injective: https://www.youtube.com/watch?v=7Ml8u7DFgAk

But I don't understand how I can use such proofs in my example. If this is not possible what is the best way to write such functions?

Answer 1

The auto keyword basically tells Idris, "Find me any value of this type". So you're liable to get the wrong answer unless that type only contains one value. Idris sees {auto x : Bool} and fills it in with any old Bool, namely False. It doesn't use its knowledge of later arguments to help it choose - information doesn't flow from right to left.

One fix would be to make the information flow in the other direction. Rather using a universe-style construction as you have above, write a function accepting an arbitrary type and use a predicate to refine it to the two options you want. This way Idris can look at the type of the preceding argument and pick the only value of IsListOrInt whose type matches.

data IsListOrInt a where
    IsInt : IsListOrInt Int
    IsList : IsListOrInt (List Int)

sum : a -> {auto isListOrInt : IsListOrInt a} -> Int
sum x {IsInt} = x
sum [] {IsList} = 0
sum (x :: xs) {IsList} = x + sum xs

Now, in this case the search space is small enough (two values - True and False) that Idris could feasibly explore every option in a brute-force fashion and pick the first one that results in a program which passes the type checker, but that algorithm doesn't scale well when the types are much bigger than two, or when trying to infer multiple values.

Compare the left-to-right nature of the information flow in the above example with the behaviour of regular non-auto braces, which instruct Idris to find the result in a bidirectional fashion using unification. As you note, this could only succeed when the type functions in question are injective. You could structure your input as a separate, indexed datatype, and allow Idris to look at the constructor to find b using unification.

data OneOrMany isOne where
    One : Int -> OneOrMany True
    Many : List Int -> OneOrMany False

sum : {b : Bool} -> OneOrMany b -> Int
sum (One x) = x
sum (Many []) = 0
sum (Many (x :: xs)) = x + sum (Many xs)

test = sum (One 3) + sum (Many [29, 43])

Predicting when the machine will or won't be able to guess what you mean is an important skill in dependently-typed programming; you'll find yourself getting better at it with more experience.

Of course, in this case it's all moot because lists already have one-or-many semantics. Write your function over plain old lists; then if you need to apply it to a single value you can just wrap it in a singleton list.