More fun with higher rank types

Quick correction to the last blog post: I actually didn’t need to use macros to get the effect of higher-rank polymorphism – it turns out that Typed Racket supports it out of the box!

In the interests of accuracy, here’s an example of using higher rank types in TR to make a function that accomplishes the sort of thing we discussed last post (use a polymorphic “template function” on lists as a basis to make instances for several different concrete types of list):

#lang typed/racket

  ([Boolean : (Listof Boolean)]
   [Integer : (Listof Integer)]
   [Float : (Listof Float)]))

(: generate-instructions ((All (a) ((Listof a) -> (Listof a)))
                          (Listof (ProgramState -> ProgramState))))

(define (generate-instructions template-func)
   (λ: ([ps : ProgramState])
     (struct-copy ProgramState ps
                  [Boolean (template-func (ProgramState-Boolean ps))]))
   (λ: ([ps : ProgramState])
     (struct-copy ProgramState ps
                  [Integer (template-func (ProgramState-Integer ps))]))
   (λ: ([ps : ProgramState])
     (struct-copy ProgramState ps
                  [Float (template-func (ProgramState-Float ps))]))))

Now there’s no type-checking error because the quantifier (“All”) is part of template-func, not generate-instructions. Let’s try it out with a template-func that, say, duplicates the top element of a list, and make sure it does what we think it does:

(: duplicate-top (All (a) ((Listof a) -> (Listof a))))
(define (duplicate-top xs)
  (match xs
    [(cons hd tl) `(,hd ,hd . ,tl)]
    ['() '()]))

(define start-state (ProgramState '(#f) '(12) '(3.14)))

(match-define `(,dup-bools ,dup-ints ,dup-floats) 
  (generate-instructions duplicate-top))

(define end-state (dup-bools (dup-ints (dup-floats start-state))))

(ProgramState-Boolean end-state)
(ProgramState-Integer end-state)
(ProgramState-Float end-state)

Running this produces:

Welcome to DrRacket, version 5.1.3 [3m].
Language: typed/racket [custom].
'(#f #f)
'(12 12)
'(3.14 3.14)

Just as expected. Cool!


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: