Re: [racket-users] unexpected behavior of parametric polymorphism in Typed Racket

[Daniel Feltey]

Sorry for the late reply to this thread, I tried to send this message
yesterday, but ran into problems with my email setup.

> I'm starting to think that my base assumption (that Typed Units are more
or
> less equivalent to ML signatures, structures, and functors) is way off.

The intent is that they are similar to ML signatures, structures, and
functors, but unfortunately, they just aren't quite there yet. I think they
support most of the uses of units you would find in the Racket codebase,
but when I was implementing them there weren't many uses of them as ways to
parameterize over different data types and I didn't make supporting that
use case a priority.

I do think that Typed Units would be significantly more useful if they
supported more of the ML module system features, but there are some
interesting questions about units and signatures with type parameters
should interact with untyped racket programs.

> The mention of `sig-type-form' in the error message suggests that it is
> possible to do this, but I'm not seeing the concrete syntax for this
> described anywhere.  Am I overlooking something?

You aren't overlooking anything. I had started trying to support
`define-type` style type alias definitions inside of signature definitions,
but at
some point this was abandoned and probably should have been removed when
support for Typed Units was added to Typed Racket. The error message here
comes from a missing set of parentheses around the list of type
declarations, but adding that doesn't fix the real problem that typed units
don't currently support type parameterization.


The documentation for typed units can be found at
http://docs.racket-lang.org/ts-reference/Typed_Units.html?q=typed%20units
I'm not sure how helpful it would be, basically only the `define-signature`
form differs in racket and typed/racket, and the typed
version of the other unit syntactic forms are mostly a subset of their
untyped versions.

I'm sorry that this probably doesn't help you solve your original problem,
I hope we can eventually improve the support for units in Typed Racket to
better match the features of ML modules.
Dan

On Tue, Nov 28, 2017 at 9:09 AM, Matthias Felleisen 
wrote:

>
> > On Nov 28, 2017, at 10:02 AM, Richard Cobbe  wrote:
> >
> > On Tue, Nov 28, 2017 at 09:43:54AM -0500, Matthias Felleisen wrote:
> >>
> >> I have forwarded your email to Daniel Felty who designed and
> implemented the typed units. I am hoping to get a response soon — Matthias
> >
> > Great, thanks.
> >
> >>> On Nov 26, 2017, at 6:11 PM, Richard Cobbe  wrote:
> >
> > 
> >
> >>> I'm starting to think that my base assumption (that Typed Units are
> more or
> >>> less equivalent to ML signatures, structures, and functors) is way off.
> >
> > Probably worth clarifying this: I'm not claiming that Typed Units *have*
> to
> > work like ML functors, merely that this is my starting assumption, since
> > they both appear to be designed to address many of the same problems.  If
> > they don't work like that, though, then I might need some additional
> > documentation.
>
>
> Yes. Units are not functors.
>
> I believe Daniel has written some documentation. Perhaps he can point us
> there.
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] unexpected behavior of parametric polymorphism in Typed Racket

[Matthias Felleisen]

> On Nov 28, 2017, at 10:02 AM, Richard Cobbe  wrote:
> 
> On Tue, Nov 28, 2017 at 09:43:54AM -0500, Matthias Felleisen wrote:
>> 
>> I have forwarded your email to Daniel Felty who designed and implemented the 
>> typed units. I am hoping to get a response soon — Matthias
> 
> Great, thanks.
> 
>>> On Nov 26, 2017, at 6:11 PM, Richard Cobbe  wrote:
> 
> 
> 
>>> I'm starting to think that my base assumption (that Typed Units are more or
>>> less equivalent to ML signatures, structures, and functors) is way off.
> 
> Probably worth clarifying this: I'm not claiming that Typed Units *have* to
> work like ML functors, merely that this is my starting assumption, since
> they both appear to be designed to address many of the same problems.  If
> they don't work like that, though, then I might need some additional
> documentation.


Yes. Units are not functors. 

I believe Daniel has written some documentation. Perhaps he can point us there. 


-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] unexpected behavior of parametric polymorphism in Typed Racket

[Richard Cobbe]

On Tue, Nov 28, 2017 at 09:43:54AM -0500, Matthias Felleisen wrote:
>
> I have forwarded your email to Daniel Felty who designed and implemented the 
> typed units. I am hoping to get a response soon — Matthias

Great, thanks.

> > On Nov 26, 2017, at 6:11 PM, Richard Cobbe  wrote:



> > I'm starting to think that my base assumption (that Typed Units are more or
> > less equivalent to ML signatures, structures, and functors) is way off.

Probably worth clarifying this: I'm not claiming that Typed Units *have* to
work like ML functors, merely that this is my starting assumption, since
they both appear to be designed to address many of the same problems.  If
they don't work like that, though, then I might need some additional
documentation.

Richard

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] unexpected behavior of parametric polymorphism in Typed Racket

[Matthias Felleisen]

I have forwarded your email to Daniel Felty who designed and implemented the 
typed units. I am hoping to get a response soon — Matthias




> On Nov 26, 2017, at 6:11 PM, Richard Cobbe  wrote:
> 
> Returning to this after a long delay...
> 
> On Sat, Nov 11, 2017 at 01:34:05PM -0500, Matthias Felleisen wrote:
> 
>>> (Context: I only actually intend to use `store' with a single type, but I
>>> want to define that type in a separate module.  Since the type's definition
>>> refers to `addr', I made `store' polymorphic to break the cyclical
>>> dependency.)
>> 
>> This of course calls for Typed Units, which are now available in Typed 
>> Racket thanks to Daniel Feltey.
>> 
>> It might be worth trying it out — Matthias
> 
> I started to take a look at this, and I'm having trouble seeing how this
> would work.  In particular, I'm not seeing how to include a type in a
> signature.  The following isn't syntactically correct:
> 
>(define-signature store^
>  Addr
>  Store
>  [empty-store : Store]
>  [alloc : (Store Integer -> (Values Store Addr))]
>  [alloc* : (Store (Listof Integer) -> (Values Store (Listof Addr)))]
>  [deref : (Store Addr -> Integer)]
>  [update : (Store Addr Integer -> Store)])
> 
> The presence of the bare `Addr' on the second line causes a syntax error,
> as one would expect from the docs.  Purely at random, I tried the
> following:
> 
>(define-signature store^
>  [Addr : Type]
>  [Store : Type]
>  [empty-store : Store]
>  [alloc : (Store Integer -> (Values Store Addr))]
>  [alloc* : (Store (Listof Integer) -> (Values Store (Listof Addr)))]
>  [deref : (Store Addr -> Integer)]
>  [update : (Store Addr Integer -> Store)])
> 
> This doesn't compile either (no surprise there), but it yields an
> interesting error message:
> 
>define-signature: expected sig-var-form or expected sig-type-form
>  at: Addr
>  in: ...
> 
> The mention of `sig-type-form' in the error message suggests that it is
> possible to do this, but I'm not seeing the concrete syntax for this
> described anywhere.  Am I overlooking something?
> 
> ;;;
> 
> Next: the signatures above only allow storing Integers in a Store.  I'd
> assumed that I'd eventually want to import the value type into the store@
> unit -- but then how do I include specify that type in store^ ?  In ML, I'd
> use a signature plus a 'with', but I don't see an equivalent to that here.
> 
> I'm starting to think that my base assumption (that Typed Units are more or
> less equivalent to ML signatures, structures, and functors) is way off.
> 
> Richard
> 
> -- 
> You received this message because you are subscribed to the Google Groups 
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] unexpected behavior of parametric polymorphism in Typed Racket

[Richard Cobbe]

Returning to this after a long delay...

On Sat, Nov 11, 2017 at 01:34:05PM -0500, Matthias Felleisen wrote:

> > (Context: I only actually intend to use `store' with a single type, but I
> > want to define that type in a separate module.  Since the type's definition
> > refers to `addr', I made `store' polymorphic to break the cyclical
> > dependency.)
>
> This of course calls for Typed Units, which are now available in Typed Racket 
> thanks to Daniel Feltey.
>
> It might be worth trying it out — Matthias

I started to take a look at this, and I'm having trouble seeing how this
would work.  In particular, I'm not seeing how to include a type in a
signature.  The following isn't syntactically correct:

(define-signature store^
  Addr
  Store
  [empty-store : Store]
  [alloc : (Store Integer -> (Values Store Addr))]
  [alloc* : (Store (Listof Integer) -> (Values Store (Listof Addr)))]
  [deref : (Store Addr -> Integer)]
  [update : (Store Addr Integer -> Store)])

The presence of the bare `Addr' on the second line causes a syntax error,
as one would expect from the docs.  Purely at random, I tried the
following:

(define-signature store^
  [Addr : Type]
  [Store : Type]
  [empty-store : Store]
  [alloc : (Store Integer -> (Values Store Addr))]
  [alloc* : (Store (Listof Integer) -> (Values Store (Listof Addr)))]
  [deref : (Store Addr -> Integer)]
  [update : (Store Addr Integer -> Store)])

This doesn't compile either (no surprise there), but it yields an
interesting error message:

define-signature: expected sig-var-form or expected sig-type-form
  at: Addr
  in: ...

The mention of `sig-type-form' in the error message suggests that it is
possible to do this, but I'm not seeing the concrete syntax for this
described anywhere.  Am I overlooking something?

;;;

Next: the signatures above only allow storing Integers in a Store.  I'd
assumed that I'd eventually want to import the value type into the store@
unit -- but then how do I include specify that type in store^ ?  In ML, I'd
use a signature plus a 'with', but I don't see an equivalent to that here.

I'm starting to think that my base assumption (that Typed Units are more or
less equivalent to ML signatures, structures, and functors) is way off.

Richard

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Re: [racket-users] unexpected behavior of parametric polymorphism in Typed Racket

[Matthias Felleisen]

Couldn’t Richard solve his second problem with the supply of a single type 
parameter to both new and alloc: 

#lang typed/racket

(define-type Addr Natural)
(define-type (Store α) (Listof α))

(: make-store (All (α) (-> (Values [-> (Store α)] [(Store α) α -> (Values 
(Store α) Addr)]
(define (make-store)
  (values (lambda () '())
  (lambda ({σ : (Store α)} {val : α})
(define addr (length σ))
(values (cons val σ) addr

(define-values (new alloc) [(inst make-store String)])

;; -

(let*-values ([(s) (new)]
  [(s a1) (alloc s "hello")]
  [(s a2) (alloc s 42)] ;; comment this out and it type checks 
  )
  s)

> (Context: I only actually intend to use `store' with a single type, but I
> want to define that type in a separate module.  Since the type's definition
> refers to `addr', I made `store' polymorphic to break the cyclical
> dependency.)

This of course calls for Typed Units, which are now available in Typed Racket 
thanks to Daniel Feltey. 

It might be worth trying it out — Matthias







> On Nov 10, 2017, at 12:10 PM, Sam Tobin-Hochstadt  
> wrote:
> 
> Your intuitions about both questions are right here.
> 
> First, type variables are only introduced into scope automatically in
> the function body for function definitions. You can use `#:forall`
> with `define` to use polymorphic types inline, but that does not allow
> you to define a polymorphic store value.
> 
> Second, you're right that subtyping allows `store` to be covariant,
> meaning that anyone can put additional kinds of things in a store. You
> can change this so that store is invariant by making the allowed
> hashtables possible mutable, changing that field to `(HashTable addr
> \alpha)`. Then your last example won't type check. However, that will
> mean you need to pick an initial store type, instead of having it
> inferred, and it will mean that a `(store Integer)` is not usable when
> you need a `(store Number)`.
> 
> Sam
> 
> On Fri, Nov 10, 2017 at 11:10 AM, Richard Cobbe  wrote:
>> I'm getting surprising results trying to define an abstract polymorphic
>> type in Typed Racket.  Could someone shed some light on this?
>> 
>> Consider the following definitions:
>> 
>>(struct addr ([ptr : Natural]))
>>(struct (α) store ([next-addr : addr]
>>   [table : (Immutable-HashTable addr α)]))
>> 
>>(: empty-store (All (α) (-> (store α
>>(define (empty-store)
>>  (store (addr 0) (make-immutable-hash null)))
>> 
>>(: alloc (All (α) (store α) α -> (Values (store α) addr)))
>>(define (alloc st v)
>>  (let ([a (store-next-addr st)])
>>(values (store (inc-addr a) (hash-set (store-table st) a v))
>>a)))
>> 
>>;; definitions of inc-addr & other store operations elided for brevity
>> 
>> I have two questions at this point, a big one and a small one.
>> 
>> Small question: it'd be nice to define empty-store to have type
>> (All (α) (store α)) -- i.e., without the eta expansion -- but I can't
>> figure out how to do this.  In particular, the following doesn't work:
>> 
>>(: empty-store (All (α) (store α)))
>>(define empty-store
>>  (store (addr 0) ((inst make-immutable-hash addr α) null)))
>> 
>> I get an error that "type name `α' is unbound", referring to the use of α
>> in the use of `inst'.  This surprises me, because section 4.8.3 (Lexically
>> Scoped Type Variables) of the Typed Racket Guide seems to say that α should
>> be in scope here.  Does that only work for function definitions?
>> 
>> Is there another way to do this without the thunk?
>> 
>> * * * * *
>> 
>> Big question: with the original version of empty-store, I get some very
>> surprising behavior.  Consider the following uses:
>> 
>>(: s (store String))
>>(define s ((inst empty-store String)))
>> 
>>(define-values (s1 addr) (alloc s 3))
>> 
>> This type-checks -- even the application of `alloc' in the last line.
>> What's going on here?  In my understanding of parametric polymorphism, this
>> can't be well-typed: α cannot be both String and Positive-Byte in the same
>> type application.  Did I overlook something in the Typed Racket manuals
>> that explains this?
>> 
>> After the final definition, `s1' has type (store (U Positive-Byte String)).
>> This does look sound to me, in that the values in the store are indeed
>> either Positive-Bytes or Strings.  But this makes it difficult to use the
>> type system to prevent clients from adding non-strings to the store.  Is it
>> possible to express that restriction in Typed Racket?
>> 
>> (Context: I only actually intend to use `store' with a single type, but I
>> want to define that type in a separate module.  Since the type's definition
>> refers to `addr', I made `store' polymorphic to break the cyclical
>> 

Re: [racket-users] unexpected behavior of parametric polymorphism in Typed Racket

[Sam Tobin-Hochstadt]

Your intuitions about both questions are right here.

First, type variables are only introduced into scope automatically in
the function body for function definitions. You can use `#:forall`
with `define` to use polymorphic types inline, but that does not allow
you to define a polymorphic store value.

Second, you're right that subtyping allows `store` to be covariant,
meaning that anyone can put additional kinds of things in a store. You
can change this so that store is invariant by making the allowed
hashtables possible mutable, changing that field to `(HashTable addr
\alpha)`. Then your last example won't type check. However, that will
mean you need to pick an initial store type, instead of having it
inferred, and it will mean that a `(store Integer)` is not usable when
you need a `(store Number)`.

Sam

On Fri, Nov 10, 2017 at 11:10 AM, Richard Cobbe  wrote:
> I'm getting surprising results trying to define an abstract polymorphic
> type in Typed Racket.  Could someone shed some light on this?
>
> Consider the following definitions:
>
> (struct addr ([ptr : Natural]))
> (struct (α) store ([next-addr : addr]
>[table : (Immutable-HashTable addr α)]))
>
> (: empty-store (All (α) (-> (store α
> (define (empty-store)
>   (store (addr 0) (make-immutable-hash null)))
>
> (: alloc (All (α) (store α) α -> (Values (store α) addr)))
> (define (alloc st v)
>   (let ([a (store-next-addr st)])
> (values (store (inc-addr a) (hash-set (store-table st) a v))
> a)))
>
> ;; definitions of inc-addr & other store operations elided for brevity
>
> I have two questions at this point, a big one and a small one.
>
> Small question: it'd be nice to define empty-store to have type
> (All (α) (store α)) -- i.e., without the eta expansion -- but I can't
> figure out how to do this.  In particular, the following doesn't work:
>
> (: empty-store (All (α) (store α)))
> (define empty-store
>   (store (addr 0) ((inst make-immutable-hash addr α) null)))
>
> I get an error that "type name `α' is unbound", referring to the use of α
> in the use of `inst'.  This surprises me, because section 4.8.3 (Lexically
> Scoped Type Variables) of the Typed Racket Guide seems to say that α should
> be in scope here.  Does that only work for function definitions?
>
> Is there another way to do this without the thunk?
>
>  * * * * *
>
> Big question: with the original version of empty-store, I get some very
> surprising behavior.  Consider the following uses:
>
> (: s (store String))
> (define s ((inst empty-store String)))
>
> (define-values (s1 addr) (alloc s 3))
>
> This type-checks -- even the application of `alloc' in the last line.
> What's going on here?  In my understanding of parametric polymorphism, this
> can't be well-typed: α cannot be both String and Positive-Byte in the same
> type application.  Did I overlook something in the Typed Racket manuals
> that explains this?
>
> After the final definition, `s1' has type (store (U Positive-Byte String)).
> This does look sound to me, in that the values in the store are indeed
> either Positive-Bytes or Strings.  But this makes it difficult to use the
> type system to prevent clients from adding non-strings to the store.  Is it
> possible to express that restriction in Typed Racket?
>
> (Context: I only actually intend to use `store' with a single type, but I
> want to define that type in a separate module.  Since the type's definition
> refers to `addr', I made `store' polymorphic to break the cyclical
> dependency.)
>
> Thanks,
>
> Richard
>
> --
> You received this message because you are subscribed to the Google Groups 
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an 
> email to racket-users+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

-- 
You received this message because you are subscribed to the Google Groups 
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.