Re: [racket-users] unexpected behavior of parametric polymorphism in Typed Racket
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 <rco...@pobox.com> 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] Alternatives to DrRacket
On Mon, Nov 27, 2017 at 09:48:16AM +, Robby Findler wrote: > It may help to disable online compilation. (Click on the little circle in > the bottom to get a menu that lets you disable it.) Ah! Thanks for the suggestion; I'll give that a try. 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
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] Alternatives to DrRacket
On Sun, Nov 26, 2017 at 03:42:14PM +, Stephen De Gabrielle wrote: > Hi, > > I’ve noticed some list members use other editors or IDE’s. > > I know two big reasons for using a complex tool is it’s stickiness factors; > normally a combination of familiarity (hence speed) with a lot of powerful > features and non-transportable customisation. > > Putting stickiness factors aside, what features in other editors/IDE’s > would you like to see in DrRacket? I generally switch back and forth between Emacs and DrRacket as appropriate for the task at hand. DrRacket is good for code navigation, but if I'm doing a lot of writing, I generally prefer emacs, largely for reasons that others have mentioned in this thread. There is one particular issue, however, that I haven't seen come up: power usage. I haven't really investigated what's going on here, but DrRacket drains the battery on my MacBook Pro quite rapidly (last experienced with DrRacket 6.11 on MacOS 10.12.latest). What's more, it appears to do this even if the app is only open in the background and I'm not actually interacting with it. So if I don't have access to AC power, I generally close DrRacket and stick with Emacs. If the DrRacket maintainers are interested, I'd be happy to help diagnose the power problem in more detail, as time permits. However, I don't really know what tests would be useful. Suggestions welcome! 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.
[racket-users] unexpected behavior of parametric polymorphism in Typed Racket
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.
