[racket] `require/typed` with a parameterized struct

From: Benjamin Greenman (blg59 at cornell.edu)
Date: Sat Dec 6 18:05:56 EST 2014

It makes no sense to ask the type system to distinguish a Tree of Integers
from a Tree of Symbols? Basically, I have an informal requirement (trees
are homogenous) from the untyped world that I want to formalize through
require/typed and check statically.

On Sat, Dec 6, 2014 at 5:40 PM, Matthias Felleisen <matthias at ccs.neu.edu>
wrote:

>
> This makes no sense. Parametric polymorphism is a syntactic concept (think
> for-all quantifier). It's sad enough that we export such things from typed
> to untyped modules (for pragmatic reasons, in violation of a fundamental GT
> assumption). -- Matthias
>
>
>
>
>
> On Dec 6, 2014, at 5:00 PM, Benjamin Greenman wrote:
>
> The typed racket reference shows how to require/typed a struct from an
> untyped program [1]. I'd like to generalize this example to a struct with a
> type parameter.
>
> Here is the code I would like to write. How can I get this to type check?
>
> #lang racket/base
>
> (module UNTYPED racket/base
>   (struct Tree (elem left right))
>   (provide (struct-out Tree)))
>
> (module TYPED typed/racket/base
>   (require/typed 'UNTYPED
>                  [#:struct (A) Tree
>                    ([elem : A]
>                     [left : Tree A]
>                     [right : Tree A])]))
>
> [1]
> http://docs.racket-lang.org/ts-reference/special-forms.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fprims..rkt%29._require%2Ftyped%29%29
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20141206/3ef4ff45/attachment.html>

Posted on the users mailing list.