Pattern matcher support for dead clauses

[wilbowma]

The following ought to type check, since there are no other constructors whose type (index) matches the input type:

#lang cur

(define-datatype Nat : Type
  (z : Nat)
  (s : (-> Nat Nat)))

(define-datatype Vec (A : Type) : (-> Nat Type)
  (nil : (Vec A z))
  (cons : (forall (a : A) (n : Nat) (Vec A n)
                  (Vec A (s n)))))

(define/rec/match head : (A : Type) (n : Nat) (Vec A (s n)) -> A
  [(cons A a n rst) => a])

I fear this requires non-trivial changes.

@pwang347, interested?

[pwang347]

Hmm, I seem to be running into this error using your example (with the minor modification of importing cur/stdlib/sugar):

map: all lists must have same size
  first list length: 1
  other list length: 2
  procedure: #<procedure:cons>

But yeah, the behaviour you describe would definitely have problems as is...

One approach could be to determine this beforehand when some parameterized type, e.g. (Vec A (s (s z))), is initialized, and in a sense, filter the constructors for the parameterized type itself. Firstly, I'm not sure if this could be done without performance implications (it would be calculated on each invocation of a parameterized type? could this be cached?), but we would generally need to solve the problem of whether each constructor is relevant to the parameterized type. I'm not familiar with how complicated the data definitions could get, but it seems like we could potentially just match the current type as a pattern against the resulting types?

E.g. (Vec A (s (s z))) matched against (Vec A (s n))) with the enclosing envs should match and therefore be considered relevant for that particular vector type, whereas (Vec A z) would fail.

What do you think about this approach? Any pitfalls?

Again, I'm worried that this doesn't work in the general case since I'm not too familiar with the syntax, and what is considered legal behaviour in define-datatype.

[wilbowma]

You'll need to pull/reset on master (we finally merged everything!). I "fixed" that bug.

That sounds about right. I don't see the potential performance issue though.

I'd probably try to write a type "equivalence" (not really equivalence, but unification, but I don't want a general, global unification system) procedure, then ensure that there is a branch for each constructor whose type (instantiated with all the right arguments) that is "equal" (in the above sense) to the type of the target of the pattern match.

[pwang347]

Are you familiar with this issue?

..\..\..\..\cur-lib\cur\curnel\cic-saccharata.rkt:41:49: application: missing argument expression after keyword in: #:unexpanded

It seems to be present in any file using #lang cur for me after merging with origin/main. Do I need to be using a different branch for turnstile or macrotypes?

[wilbowma]

Yes, you'll need to update to Turnstile's main branch. You can probably do this by uninstalling turnstile etc, then just do raco pkg install from cur-lib and it will pull the right dependencies.