Conversation

Nov 29, 2021

Does anyone know why Idris 2 can’t figure this out? I have to explicitly tell it that xs matches _::_, even though it knows xs can’t match Nil (because it’s in the wrong case) (This also happens with case..of)

last : Vect (S n) a -> a
last (x :: Nil) = x
last (_ :: xs) = last xs

read image description

ALT

eleanor

@zornsllama

Nov 29, 2021

The simplest answer is just “it isn’t that smart” but I’m wondering if there’s a more detailed answer explaining whys

Brendan Zabarauskas

@brendanzab

Nov 29, 2021

Looks similar to the ‘forced patterns’ feature

@OwoTizusa

was working on for Aya? For this specific issue, you might need to help Idris along by matching on the implicit `n` parameter. This might let you remove the redundant case. twitter.com/OwoTizusa/stat

This Tweet is unavailable.

eleanor

@zornsllama

Nov 29, 2021

For the record if I make it `last (_::xs@(_::_))` then Idris works it out just fine. I’ll try matching on the implicit parameter tomorrow!

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

eleanor

@zornsllama

Nov 30, 2021

so the top definition works, but if I try to match on the implicit parameter (last') Idris yells at me because `n` is only accessible at compile time :(

$last : (n : Nat) -> Vect (S n) a -> a last Z (x::Nil) = x last (S n) (_::xs) = last n xs last' : Vect (S n) a -> a last' {n} xs = last n xs$

read image description

ALT

eleanor

@zornsllama

Nov 30, 2021

Idris also doesn't like doing it directly, it says: Error: While processing left hand side of last. Can't match on S ?_ (Erased argument).

$last : Vect (S n) a -> a last {n=Z} (x::Nil) = x last {n=S _} (_::xs) = last xs$

read image description

ALT

eleanor

@zornsllama

Nov 30, 2021

the definition (a : Nat) -> Vect (S n) a -> a works but is much uglier than the workaround I had before imo

Replying to

and

Ohhhh so idris erases implicit variables by default I think. Ie. you can't match on them if they are erased at runtime! I believe there is a way to make these usable at runtime though, lemme check.

11:03 AM · Nov 30, 2021Twitter Web App

Replying to

and

bind it yourself

Ahh yeah, what I said here: twitter.com/brendanzab/sta Think the trick is knowing that Idris _generalises_ this: last : Vect (S n) a -> a to this: last : {0 n : Nat} -> Vect (S n) a -> a where as we really want: last : {n : Nat} -> Vect (S n) a -> a

Quote Tweet

Brendan Zabarauskas

@brendanzab

· Nov 30, 2021

Replying to @brendanzab @zornsllama and @OwoTizusa

On I think it is just `{n : Nat} -> Vect (S n) a -> a` - it's the lowercase, auto-generalised variables it automatically sets to be 'erased' (ie. to a 0 multiplicity).

Show replies

Replying to

and

On I think it is just `{n : Nat} -> Vect (S n) a -> a` - it's the lowercase, auto-generalised variables it automatically sets to be 'erased' (ie. to a 0 multiplicity).