Occurrence typing with polymorphic union types

Question

Suppose I want to convert the following untyped code into typed racket. These functions are inspired by SICP where they show how a data structure can be constructed purely from functions.

(define (make-pair x y)
    (lambda (c)
        (cond
            ((= c 1) x)
            ((= c 2) y)
            (error "error in input, should be 1 or 2"))))

(define (first p) (p 1))
(define (second p) (p 2))

To convert it straight to typed racket, the return value of the make-pair function seems to be (: make-pair (All (A B) (-> A B (-> Number (U A B))))). And following this, the type of first should be (: first (All (A B) (-> (-> Number (U A B)) A))). However, while implementing the function we can't call (p 1) directly now because we need some sort of occurrence typing to make sure first returns only of type A. Changing the return type of first to (U A B) works but then the burden of occurrence typing goes on the user and not in the API. So in this scenario how can we use occurrence typing inside first (that is, how to use a predicate for type variable A) so that we can safely return only the first component of the pair?

UPDATE

I tried an approach which differs a bit from above and requires the predicates for A and B to be supplied as arguments to make-pair function. Below is the code:

#lang typed/racket


(define-type FuncPair (All (A B) (List (-> Number (U A B)) (-> A Boolean) (-> B Boolean))))

(: make-pair (All (A B) (-> A B (-> A Boolean) (-> B Boolean) (FuncPair A B))))
(define (make-pair x y x-pred y-pred)
    (list
        (lambda ([c : Number])
            (cond
                ((= c 1) x)
                ((= c 2) y)
                (else (error "Wrong input!"))))
        x-pred
        y-pred))

(: first (All (A B) (-> (FuncPair A B) Any)))
(define (first p)
    (let ([pair-fn (car p)]
          [fn-pred (cadr p)])
        (let ([f-value (pair-fn 1)])
            (if (fn-pred f-value)
                f-value
                (error "Cannot get first value in pair")))))

However, this fails in the check (fn-pred f-value) condition with error expected: A given: (U A B) in: f-value

Alex Knauth Alex Knauth · Accepted Answer · 2016-08-31T13:49:16

From the untyped code at the start of your question, it seems like a pair of A and B is a function that given 1, gives back A, and given 2, gives back B. The way to express this type of function is with a case-> type:

#lang typed/racket

(define-type (Pairof A B)
  (case-> [1 -> A] [2 -> B]))

The accessors can be defined the same way as your original untyped code, just by adding type annotations:

(: first : (All (A B) [(Pairof A B) -> A]))
(define (first p) (p 1))
(: second : (All (A B) [(Pairof A B) -> B]))
(define (second p) (p (ann 2 : 2)))

The type of the constructor should be:

(: make-pair : (All (A B) [A B -> (Pairof A B)]))

But the constructor doesn't quite work as-is. One thing wrong with it is that your else clause is missing the else part of it. Fixing that gives you:

(: make-pair : (All (A B) [A B -> (Pairof A B)]))
(define (make-pair x y)
  (lambda (c)
    (cond
      [(= c 1) x]
      [(= c 2) y]
      [else (error "error in input, should be 1 or 2")])))

This is almost right, and if typed racket were awesome enough, it would be. Typed racket treats equal? specially for occurrence typing, but it doesn't do the same thing for =. Changing = to equal? fixes it.

(: make-pair : (All (A B) [A B -> (Pairof A B)]))
(define (make-pair x y)
  (lambda (c)
    (cond
      [(equal? c 1) x]
      [(equal? c 2) y]
      [else (error "error in input, should be 1 or 2")])))

Ideally occurrence typing should work with =, but perhaps the fact that things like (= 2 2.0) return true makes that both harder to implement and less useful.

Occurrence typing with polymorphic union types

1 Answers