Add totality checking

[wilbowma]

This PR replaces #103.

[wilbowma]

Opened this to easily see conflicts/Travis in one place.

Looks like we're getting false negatives from Travis. It passes, but I see the following in the logs and when I run Poly-pairs.rkt myself.

raco test ../../../cur/cur-test/cur/tests/ntac/software-foundations/Poly-pairs.rkt

Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
raco test: "../../../cur/cur-test/cur/tests/ntac/software-foundations/Poly-pairs.rkt"
raco test: @(test-responsible '(wilbowma stchang))
32 tests passed

[wilbowma]

cc @pwang347

[pwang347]

Opened this to easily see conflicts/Travis in one place.

Looks like we're getting false negatives from Travis. It passes, but I see the following in the logs and when I run Poly-pairs.rkt myself.

raco test ../../../cur/cur-test/cur/tests/ntac/software-foundations/Poly-pairs.rkt

Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
Failed to determine type of #<syntax temp105>
ERROR: #(struct:exn:fail:syntax temp105: unbound identifier;
 also, no #%top syntax transformer is bound
  in: temp105 #<continuation-mark-set> (#<syntax temp105>))
raco test: "../../../cur/cur-test/cur/tests/ntac/software-foundations/Poly-pairs.rkt"
raco test: @(test-responsible '(wilbowma stchang))
32 tests passed

I made a brief comment about this in #103:

Currently there is a bit of log spewing from get-typeof in stdlib\pattern-tree.rkt for certain files. This is because it doesn't know how to handle implicitly defined constructors, especially trickier cases like :: which supports infinite nesting (this is the main TODO that I'm aware of)

I had it left as is, but maybe it might be preferred to silence it and add a TODO instead. (The error itself is technically not wrong as it failed to produce a type, but there are a few specific cases where it's unhandled at this point)

[wilbowma]

Missed that, thanks!

[pwang347]

Also if I remember correctly, the behaviour of untyped variables in totality checking is just an automatic pass, so totality checking should be skipped for any and all variables facing such an issue (potentially a partial totality check, whew that sounded weird)

[pwang347]

https://github.com/wilbowma/cur/pull/105/commits/4b0faf18bf121c0b10d55665d885128a813db30a#diff-286c6976832f9a510328591747a86955R125

I think I also wanted to call subst-tmp on the terms here whoops

[wilbowma]

Also if I remember correctly, the behaviour of untyped variables in totality checking is just an automatic pass, so totality checking should be skipped for any and all variables facing such an issue (potentially a partial totality check, whew that sounded weird)

Didn't really understand this comment. Do you mean if we have a variable missing a type annotation, totality checking will automatically succeed?

[pwang347]

So say we match on two variables, e.g. a, b Where both are intended to be Nat, but for whatever reason b wasn't able to be labelled. The following match cases should pass:

[z z]
[(s x) z]

But the following should not:

[z z]
[z (s x)]

This is usually not a problem for positional arguments that are passed in by the user (in this case there is no ambiguity on the type), but it becomes an issue when we generate temporaries while flattening the patterns, since the type of the temporaries are inferred from the nested match expressions.

[wilbowma]

Hm. That's a strange behavior and makes me worry about type soundness. Will have to think on it.

[pwang347]

See updated comment above! Yeah, can potentially lead to some false negatives. I think I was trying to play it safe with backwards compat in this case.

[wilbowma]

Normally a good call, but in a dependently typed language, soundness trumps backwards compatibility.

[pwang347]

Makes sense. For reference, the behaviour is created here: https://github.com/wilbowma/cur/pull/103/files#diff-df1a362f622a4c434e1c207377ada588R23 (get-constructors-metadata returns false if no type information is inferred, which implies there's nothing to check)

[wilbowma]

Thanks!

[wilbowma]

Looks like the first failing definition is this one:

(define/rec/match split_ : [X : Type] [Y : Type] (list (prod X Y))
  -> (prod (list X) (list Y))
  [nil => (pair (nil* X) (nil* Y))]
  [(:: (pair m n) xs)
   => (pair (:: m (fst (split_ X Y xs)))
            (:: n (snd (split_ X Y xs))))]
  #:type-aliases ([pair = pair* 2]))

It ought to be total, so this is a false positive resulting from lack of type information that we ought to be able to recover.

[wilbowma]

Okay, I think I'm declaring this out of scope for the current PR. The root cause of the problem seems to be poor handling or implicits, but the implementation of implicits is flawed and at the root of the problem.

[pwang347]

Hey I'm still out doing a big move out from my apartment, but I'll try to address all your TODO comments when I'm back.

Edit: probably won't be back until close to midnight

[wilbowma]

No worries, I'm still reviewing and thinking about the code. Not sure how many will remain. I'm removed at least one as I understood the code better.

[wilbowma]

I pushed two major changes. One replaced the C-hash implementation with a custom immutable hash. This seemed to work. The second replaced the constructor metadata implementation. This kind of works, but there's a few differences in interface that break in a few places that I haven't finished debugging. Will continue later this week.

[wilbowma]

Okay I'm feeling pretty good about my understanding of the code now. The only major thing I want to change is the interface to inductive constructors. I made some changes, but plan to make some more which should take some O(n) checks down to O(1).

[pwang347]

Okay I'm feeling pretty good about my understanding of the code now. The only major thing I want to change is the interface to inductive constructors. I made some changes, but plan to make some more which should take some O(n) checks down to O(1).

Sounds great, thanks William!

[wilbowma]

Closed by 9b3dc826660a21fdd14690a18cad0eaf5e301086

[stchang]

Is something like this supposed to work?

(define/rec/match test : (X : Type) X -> X
  [x => x])

It's currently rejected by total? because X is not inductive.

[wilbowma]

I would say "no", since we can't know anything about that type, such as what it's constructors are. What if at run-time, you provide a function?

While this specific case isn't a problem since it's just the identity, the semantics should be similar to eliminators, and we wouldn't ever be able to eliminate that.

[stchang]

So Coq would reject this? (cant get Coq running at the moment)

[dmelcer9]

Is there an equivalent to def/rec/match in coq?

[wilbowma]

def/rec/match is meant to mimic Fixpoint in Coq, IIRC (which requires that you then use match in the body)

[dmelcer9]

But in

match foo, bar with ...

Both foo and bar need to be inductive vars, while the first line of a def/rec/match is serving that role here.

[wilbowma]

Right. And the definition using def/rec/match is being rejected because the equivalent of bar isn't inductive.