[racket-dev] Experimenting with generics in TR

From: Neil Toronto (neil.toronto at gmail.com)
Date: Mon Feb 11 14:13:35 EST 2013

On 02/10/2013 06:55 AM, Sam Tobin-Hochstadt wrote:
> What is the type of `ops-hash` intended to be here?

There's no valid Typed Racket type. It represents an extensible mapping 
from types to ring operations on those types.

Using `case->', it's not too hard to make a mapping from symbols to ring 
operations; e.g.

   (case-> ('integer -> (ring-ops Integer))
           ('polynomial -> (ring-ops (polynomial T))))
           ...)

But everything that uses a function with that type has to itself have 
corresponding cases, so I can't write a function with this type:

   ring+ : (All (A) ((ring-member A) (ring-member A) -> (ring-member A)))

It would have to have a huge `case->' type as well, which rules out 
separate compilation: `ring+' could operate only on rings it statically 
knows about.

This program represents the closest I've gotten to generics using a hash 
table of types to ring operations:


#lang racket/load

(module ring-types typed/racket
   (provide (all-defined-out))

   (struct: (A) ring-member ([value : A] [ops-name : Symbol]))

   ;; Can't use a struct; gives this error when using `set-ring-ops!':
   ;;   struct/dc: expected chaperone contracts, but field zero has
   ;;   #<barrier-contract>
   ;; Fields: zero, add, negate, multiply
   (define-type (ring-ops A) (List A (A A -> A) (A -> A) (A A -> A))))


(module dispatch racket
   (require 'ring-types)

   (provide set-ring-ops! get-ring-ops)

   (define ops-hash (make-hasheq))

   (define (set-ring-ops! name ops)
     (hash-set! ops-hash name ops))

   (define (get-ring-ops name)
     (hash-ref ops-hash name (λ () (error 'get-ring-ops
                                          "unregistered ring ~a"
                                          name)))))

(module defs typed/racket
   (require 'ring-types)

   (require/typed
    'dispatch
    [set-ring-ops!  (All (A) (Symbol (ring-ops A) -> Void))]
    [get-ring-ops   (All (A) (Symbol -> (ring-ops A)))])

   (set-ring-ops! 'integer (list 0 + - *))

   ((inst get-ring-ops Integer) 'integer))

(require 'defs)


I (expectedly) get this error:

   get-ring-ops: broke its contract
    promised: A7
    produced: #<A6>

with ((inst get-ring-ops Integer) 'integer) highlighted.

Obviously, the contract system can't prove that the (ring-ops A) it 
returns has the right type. That's why I asked about an 
ultra-super-secret back door.

FWIW, I've managed to get something less than decent working just using 
Typed Racket, by including a (ring-ops A) in every (ring-member A); i.e.

   (struct: (A) ring-member ([value : A] [ops : (ring-ops A)]))

But the function types in `ring-ops' make `ring-member' invariant. I 
want (Polynomial Integer) <: (Polynomial Real).

Neil ⊥


> On Sat, Feb 9, 2013 at 9:27 PM, Neil Toronto <neil.toronto at gmail.com> wrote:
>> I'd like to play around with implementing generics or type classes in Typed
>> Racket, but without changing its internals, just to see what it takes. I
>> think I could get something pretty decent working if I could get the
>> following program to type:
>>
>>
>> (define ops-hash (make-hasheq))
>>
>> (: set-ring-ops! (All (A) (Symbol (ring-ops A) -> Void)))
>> (define (set-ring-ops! name ops)
>>    (hash-set! ops-hash name ops))
>>
>> (: get-ring-ops (All (A) ((ring-member A) -> (ring-ops A))))
>> (define (get-ring-ops x)
>>    (define name (ring-member-ops-name x))
>>    (hash-ref ops-hash name (λ () (error 'get-ring-ops
>>                                         "unregistered ring ~a"
>>                                         name))))
>>
>>
>> Of course, I can't. In fact, I can't get this to work by writing
>> `set-ring-ops!' and `get-ring-ops' in untyped Racket and importing them
>> using `require/typed', because the contract system can't prove that the `A'
>> in `get-ring-ops' is the same as the `A' in `set-ring-ops!'.
>>
>> Is there a secret, hidden escape hatch that would allow me to get functions
>> with these types and behaviors?
>>
>> Neil ⊥
>> _________________________
>>   Racket Developers list:
>>   http://lists.racket-lang.org/dev


Posted on the dev mailing list.