Typed Racket: Creating generic types with define-type

Question

I'm trying to get a bit into Typed Racket, but I'm having some trouble getting an (admittedly rather constructed) experiment to work.

This is what I originally had:

#lang typed/racket

(: generate-list
   (All (A)
   ((A -> A) (Integer -> A) Integer -> (Listof A))))

(define (generate-list function location-function num-items)
  (let: loop : (Listof A)
    ((count : Integer 0)
     (result : (Listof A) (list)))
    (if (>= count num-items)
        (reverse result)
        (loop (+ count 1)
              (cons (function (location-function count)) result)))))

; ---------------------------------
(: f (Number -> Number))
(define (f x) (* x x))

(: locf (Integer -> Number))
(define (locf x) x)
; ---------------------------------

(displayln (generate-list f locf 10))

Which has the output:

(0 1 4 9 16 25 36 49 64 81)

Which is nice. Then I figured I could make this a bit better documented by giving the function and location-function a defined type:

#lang typed/racket

(define-type (ListGenFunction A) (A -> A))
(define-type (ListGenLocFunction A) (Integer -> A))

(: generate-list
   (All (A)
        (ListGenFunction ListGenLocFunction Integer -> (Listof A))))

(define (generate-list function location-function num-items)
  (let: loop : (Listof A)
    ((count : Integer 0)
     (result : (Listof A) (list)))
    (if (>= count num-items)
        (reverse result)
        (loop (+ count 1)
              (cons (function (location-function count)) result)))))

; ----------- Numbers! ------------
(: f ListGenFunction)
(define (f x) (* x x))

(: locf ListGenLocFunction)
(define (locf x) x)
; ---------------------------------

(displayln (generate-list f locf 10))

Now here's where the problems start (and I really hope some experienced Typed Racketeers aren't facepalming too hard right now). For one, the type checker gives me an error on the line where I define f. The message is rather lengthy, but it's basically: "Type Checker: No function domains matched in function application: Types: ... in: (* x x)". I thought I defined a type that has one parameter of a generic type A that returns a generic type A? Wouldn't (* x x) work? Or is there some need to "tag" the type? (Like in C++-like languages where it's list<int> for example)

On top of that: Now my type-definition for the function generate-list has a return type of "(Listof A)". But that A is not at all declared to be the same A that the parameters with the types ListGenFunction and ListGenLocFunction expect. I kind of want to make that connection, however, so that anyone who uses that function can be sure that the types of his provided functions match the type of the returning list items.

How do I do this correctly?

PS: I'm not sure if I described my intention in the last paragraph so that anyone can understand it. But if you take some generic pseudo-C++-like code, I want to get the following:

list<T> generate-list(LGF<T> f, LGLF<T> locf, int count) { ... }

So that all T's are exactly the same.

Sam Tobin-Hochstadt Sam Tobin-Hochstadt · Accepted Answer · 2013-06-21T14:25:29

There are two problems here, both of which stem from the same confusion. You're using a generic type, ListGenFunction, without telling Typed Racket (or the reader of your program) what particular type you're using it with.

For example, f isn't an arbitrary ListGenFunction, it's a ListGenFunction that works specifically on numbers. So you should write:

(: f (ListGenFunction Integer))

and

(: locf (ListGenLocFunction Integer))

Similarly, you should give generate-list a type like this:

(: generate-list
   (All (A)
     ((ListGenFunction A) (ListGenLocFunction A) Integer -> (Listof A))))

This is just like how you explicitly say that you're producing a (Listof A), not just a Listof.

Typed Racket: Creating generic types with define-type

1 Answers