Totality and Pattern Matching on Types in Idris2

[Nicolas Alexander Schmidt]

Hi,


for a project I'm currently working on, I need to be able to talk about
subuniverses of types. Before, I used Tarski-style universes (i.e. an
abstract type `idx` of names together with an interpretation function
`el : idx -> Type`), but this turned out to be quite cumbersome.
Therefore, I now switched to predicates, but unfortunately I encountered
a problem.

This problem is illustrated by the following interface, whose
implementation Idris 2 complains to be non-covering.


    interface Foo (p : Type -> Type) where
      bar : {a : _} -> p a => a
   
    OnlyInt : Type -> Type
    OnlyInt Int = ()
    OnlyInt _ = Void
   
    Foo OnlyInt where
      bar {a=Int} = 0


Is there a way to complete this implementation? I have the feeling there
isn't, as `Type` isn't an inductive type, but maybe I miss something
obvious.


Best,

Nicolas

[Denis Buzdalov]

Hi Nicolas,

 

    Foo OnlyInt where
      bar {a=Int} = 0

The function `bar` that you give is really non-covering. It does not cover all possible `a`s and it is right that the compiler can't figure out the idea that the left case has `Void` as a parameter. `Void` itself does not mean anything to the compiler. `impossible` cases in the pattern match are those cases that produce a unification error.

If you would write the rest pattern matc case as `bar {a=x} = ?foo`, you'll see that `?foo` hole has type `x`, as expected. You expect (as a human) that in this case, the `auto`-argument would be `Void` and thus we can use `absurd` for that.

Let's see and pattern match on it: `bar {a=x} @{o} = ?foo`. If you see the context of `?foo` hole, you'll see that `o` has type `OnlyInt x`. Since `x` is just an unknown `Type`, a function application `OnlyInt x` is not reduced to `Void` as you want. Idris does not take into account the fact that you have already pattern matched on `a` previously. That's why you don't have any ability to use `absurd` since you don't have any `Void` as an argument.

The way I see to deal with it is the following. You need `OnlyInt` to be a GADT that you can pattern match on, to get your beloved `Void`. For example:

```idris

data OnlyInt : Type -> Type where
  NiceCase : OnlyInt Int
  BadCase  : Void -> OnlyInt x

Foo OnlyInt where
  bar {a=Int} @{NiceCase}  = 0
  bar {a=x}   @{BadCase y} = absurd y

```

(by the way, you can omit `{a=x}`)

In this case once you've matched on `a` you can also match on `OnlyInt`. And since you've matched the `Int` case, the rest case (`BadCase` constructor) has `Void` inside it, thus you can use it to pass to `absurd`.

I hope it helped.

Denis

[Nicolas Alexander Schmidt]

Hi Denis,


thank you very much for your very nice answer, it definitely helps! I
completely forgot about the possibility of using GADTs to construct type
families---my bad!

Your solution makes sense to me, except that I don't completely
understand the necessity of the constructor `BadCase`. That is, one
might naively think that

```idris
data OnlyInt : Type -> Type where
  NiceCase : OnlyInt Int

Foo OnlyInt where
  bar {a=Int} @{NiceCase}  = 0

```


should also do the trick, as this is clearly an exhaustive pattern match
on the auto-implicit variable. However if you try that, the type checker
gives the familiar complaint about non-coverage. I am not entirely sure
why that is or why it works with two constructors.

Btw, I actually made a mistake: the predicate should of course not be of
type `Type -> Type` but rather of type `Type -> Prop` where by `Prop` I mean

```idris

IsProp : Type -> Type
IsProp ty = (x : ty) -> (y : ty) -> (x = y)

Prop : Type
Prop = Subset Type IsProp

```.

My mistake was in thinking that since Idris' type system has UIP, all
types are propositions anyway, but of course that's not true: types are
only sets. Fortunately, your solution can be adapted easily:

```idris

data OnlyInt' : Type -> Type where

   NiceCase : OnlyInt' Int

   BadCase : Void -> OnlyInt' x

OnlyInt'_is_prop : (x : OnlyInt' ty) -> (y : OnlyInt' ty) -> x = y

OnlyInt'_is_prop {ty=Int} NiceCase NiceCase = Refl

OnlyInt'_is_prop (BadCase pf) y = absurd pf


OnlyInt : Type -> Prop

OnlyInt ty = Element (OnlyInt' ty) OnlyInt'_is_prop

```.

It's a bit verbose, but it works. Again, many thanks.


Best,
Nicolas


Am 27.01.21 um 10:53 schrieb Denis Buzdalov:

> --
> You received this message because you are subscribed to the Google
> Groups "Idris Programming Language" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to idris-lang+...@googlegroups.com
> <mailto:idris-lang+...@googlegroups.com>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/idris-lang/CAP77jwW%3DeSw%3DTzwVup1d8aQOrg_TNKAtxC3Lpbd1N1a1pa3mnA%40mail.gmail.com
> <https://groups.google.com/d/msgid/idris-lang/CAP77jwW%3DeSw%3DTzwVup1d8aQOrg_TNKAtxC3Lpbd1N1a1pa3mnA%40mail.gmail.com?utm_medium=email&utm_source=footer>.

[Denis Buzdalov]

Nicolas,

Your solution makes sense to me, except that I don't completely
understand the necessity of the constructor `BadCase`. That is, one
might naively think that


```idris
data OnlyInt : Type -> Type where
  NiceCase : OnlyInt Int

Foo OnlyInt where
  bar {a=Int} @{NiceCase}  = 0
```


should also do the trick, as this is clearly an exhaustive pattern match
on the auto-implicit variable. However if you try that, the type checker
gives the familiar complaint about non-coverage. I am not entirely sure
why that is or why it works with two constructors.

This is because of how the totality checker works with types that are present at runtime.

You can look at https://github.com/idris-lang/Idris2/issues/402 for explanation.

TLDR, if you'd add a 0-quantity to the `{a : _}` argument of your function, everything would work at you'd expect:

```idris

interface Foo (p : Type -> Type) where

  bar : {0 a : _} -> p a => a

data OnlyInt : Type -> Type where
  NiceCase : OnlyInt Int

Foo OnlyInt where

  bar @{NiceCase} = 0

```

However, for inductive types (i.e. defined with a number of constructors) your original approach with runtime data also works. For example, if you use `Nat`s instead of `Type`s, everything works with a runtime parameter:

```idris

data X : Nat -> Type where
  X10 : X 10

bbar : {a : _} -> X a -> Int
bbar {a=10} X10 = 1

```

This is because the totality checker can say for sure that there are no such else `a`s that match `10` which came from the `X10`'s type.

Denis

[Nicolas Alexander Schmidt]

Hey Denis,

> Nicolas,

>
> This is because of how the totality checker works with types that are
> present at runtime.
> You can look at https://github.com/idris-lang/Idris2/issues/402 for
> explanation.

thanks for the link and

>
> TLDR, if you'd add a 0-quantity to the `{a : _}` argument of your
> function, everything would work at you'd expect:
>
> ```idris
> interface Foo (p : Type -> Type) where
>   bar : {0 a : _} -> p a => a
>
> data OnlyInt : Type -> Type where
>   NiceCase : OnlyInt Int
>
> Foo OnlyInt where
>   bar @{NiceCase} = 0
> ```

this alternative solution. I like it, it's much less verbose!

Best,

Nicolas