I’m having some trouble with predicates in typed racket.

I have a Listof String, and I’d like to convert this to a List String String (since I know that the list only has two elements).

It would be easy enough to write a function with a type like (-> (Listof String) (List String String)), but I thought it would be nicer if I could have a predicate like (-> Any Boolean : (List String String)), or even (-> (Listof String) Boolean : (List String String)).

I could do this with define-predicate:

(define-predicate 2list-foo? (List String String)) ;; (in repl) ;; > 2list-foo? ;; - : (-> Any Boolean : (List String String)) However, what I’d really like is a polymorphic predicate function with a type like the following:

(All [A] (-> (Listof A) Boolean : (List A A))) It doesn’t appear that I am able to do this with the define-predicate function, since it always assumes the domain of the predicate is Any, so I have no place to introduce the polymorphic type variable.

I tried to write a function like this myself, and I can do it without the proposition:

(: 2list-bar? (All [A] (-> (Listof A) Boolean))) (define (2list-bar? lst) (if (eq? (length lst) 2) #t #f)) However, if I try to add the proposition I want, it gives me an error:

(: 2list? (All [A] (-> (Listof A) Boolean : (List A A))) (define (2list? lst) (if (eq? (length lst) 2) #t #f)) Here’s the error:

mismatch in proposition ; expected: ((: lst (List A A)) \| (! lst (List A A))) ; given: (Bot \| Top) ; in: #f It doesn’t seem to help if I remove the polymorphic A and just make it concrete over String.

I have a couple questions:

1. Why doesn’t this work?
2. What is the error trying to tell me?
3. I’m guessing that eq? and length just don’t give enough info to the type-checker to prove this proposition. Is there some way to get this to work?
4. I also tried to work around this with cast, and that doesn’t seem to work either. Is there some sort of unsafe-cast function? It would be nice to be able to tell the type-checker “Hey, trust me on this, I know what I’m doing”.

Oh, also, I’m completely new to typed racket (and racket as well), so I could just be doing something dumb.

Have you tried writing it out more explicitly, with car, cdr, null?

That would be my first try

@samth Good idea.

I tried that, and I still get a mismatch in proposition error:

(: 2list? (-> (Listof String) Boolean : (List String String))) (define (2list? lst) (if (null? lst) #f (let ([xxx : (Listof String) (cdr lst)]) (if (null? xxx) #f #t))))

Oh, I wasn’t sure whether or not null? would be sufficient here, so I tried to rewrite it with pair? , and it still appears to not be working.

This appears to be the paper on how occurrence typing works, although after a quick skim through it, it doesn’t seem to have an example close to what I’m after: https://www2.ccs.neu.edu/racket/pubs/icfp10-thf.pdf

There is also a dissertation on typed racket. Maybe this is the thing I need to read. It seems to go into more depth(?) than either the typed racket guide or reference: https://www2.ccs.neu.edu/racket/pubs/dissertation-tobin-hochstadt.pdf

Oh, I figured this out. This is significantly easier than I thought:

(: 2list? (All [A] (-> (Listof A) Boolean : (List A A)))) (define (2list? lst) (and (pair? lst) (pair? (cdr lst)) (null? (cddr lst)))) My guess is that my main problem is that Typed Racket wasn’t able to follow the flow of the variables with the let bindings I was using. I guess that makes sense.