add predicates for concrete-only types

[AlexKnauth]

So that assert-type can work with concrete types like CNat.

I have a question. Is there any chance this could lead to unsoundness? For base types I don't think so, but I vaguely remember discussing this and deciding to only add predicates for possibly-symbolic types. Was that because it caused some problem that I'm not seeing now? Or was it just not necessary then?

[stchang]

I implemented a similar thing in my local and you should merge this in but I think it indicates a larger problem.

In particular, non-lifted predicates like these dont affect what the solver has to do, so they are effectively dynamic concrete checks on a function argument, which a type system is supposed to get rid of!

The problem I think is that our type system is too lax in letting concrete values become symbolic. So we need to generate checks like this to refine the type back to something concrete (because for our type system to be useful, it must preserve concreteness for as long as possible). But ideally, we should just preserve the concrete type in the first place.

Here's a pattern I run into a lot:

(define (f [x : Int]) -> Int x)
(f 4)

The (f 4) becomes symbolic when it is obviously still concrete. This is related to #5 and a case-lambda-like form would help with this. I guess what I want is the ability to define functions that are generic over concrete/symbolicness.

Does that make sense? Have you run into situations like this? Is that what you are using these asserts for?

[AlexKnauth]

That makes sense, uses of assert-type is this way will always be a sign of our type system being not precise enough. However, I think that it will still be needed since there will probably always be places where the type system isn't precise enough for certain programs.

Though some of the situations I've come across have been situations where it's a CInt that it can't prove is a CNat. That's also a problem of the type system not being precise enough, but the concreteness is fine.

[stchang]

Actually maybe case-lambda is not needed. Maybe some form of concreteness polymorphism? eg, where X = a type variable representing a concrete or symbolic constructor?

(define (f {X} [x : (X CInt)]) -> (X CInt)
   (+ x 1))

[AlexKnauth]

We wrote this comment above assert-type:

;; TODO: assert-type wont work with unlifted types
;; but sometimes it should, eg in with for/all lifted functions
;; - but this means we need to lift a pred (eg string?) and associate it with the newly lifted type 

If a predicate, say concrete-string? is lifted using for/all,

(define (string? v)
  (for/all ([v v]) (concrete-string? v)))

Then string? cannot be a predicate for CString. If we use occurrence typing on this definition, we have to make sure it doesn't allow a #:+ CString filter through the for/all. It can be a predicate for (U CString) though.

[AlexKnauth]

Types for container values like structs couldn't work like normal. If there was a struct declaration like

(struct foo ([a : CInt]) #:transparent)

Then values of this shape would have the type CFoo:

(foo CInt) : CFoo

And values of this shape would have the type (U CFoo):

(union (foo CInt) ...) : (U CFoo)

However these values would be merged into

(foo Int) : (U CFoo)

Now that's fine as a (U CFoo), but not fine as a CFoo, even though an unlifted foo? would return true on it. So unless we do something different wrt merging, we can't use concrete predicates to distinguish types that could represent container values.

(Note: I used the typed racket convention for structure types, where Foo is the type itself, and not a type constructor to use as (Foo A). However, the typed racket convention is actually very useful for using occurrence typing on wrapped higher-order values, and it remains sound because foos with other types are impossible to construct. Rosette's merging breaks that slightly, because foos can be constructed with symbolic versions of the types. However that should be fine as long as we make sure that that (foo (union A ...)) values are never given the type CFoo.)

[stchang]

I do not think it's a good idea to use CFoo as the type instead of (CFoo CInt).

From what I've seen, it's a common idiom to rely on the the container remaining concrete, while the elements will be possibly symbolic (and Emina confirmed this last week).

This means that we should not conflate (ConcreteContainer SymbolicX) and (SymbolicContainer ConcreteX) as just SymbolicContainer.

Btw, the current typed definition of for/all seems wrong? The first clause is supposed to match the symbolic cases, but should it have an ellipses after the τ_x? So (~U* τ_x ...) instead of (~U* τ_x).

[AlexKnauth]

Re: The current rule for for/all:

What it currently does is unsound. For example when given PosInt it will bind the variable as CPosInt even if it ends up as a symbolic constant. I'm not sure how to do this correctly without being way too conservative.

It also doesn't preserve concrete types. For example in Ocelot there are places where (while typechecking a case->) for/all is given a concrete type, and the body has a concrete type, so the whole thing should have a concrete type, but instead it's wrapped in a symbolic union. Was that a mistake?

Update: fixed by #13

[AlexKnauth]

Superceded by #17.