I'm confused, Sam. Is the example with the indirect struct less problematic somehow? Or should it be failing? Carl Eastlund -- WARNING! Poorly-typed cell phone email precedes. <div class="gmail_quote">On Apr 11, 2013 7:23 AM, "Sam Tobin-Hochstadt" <<a href="mailto:samth@ccs.neu.edu">samth@ccs.neu.edu</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> The reason this doesn't work is that non-regular datatypes require significantly more algorithmic complexity to avoid non-termination/be correct. In particular, I don't know of a subtyping algorithm for non-regular datatypes. Sam On Thu, Apr 11, 2013 at 12:58 AM, Eric Dobson <<a href="mailto:eric.n.dobson@gmail.com">eric.n.dobson@gmail.com</a>> wrote: > So it looks like that you need an indirection struct, here is a simple example. > > #lang typed/racket > > > (struct: (a) Indirect ((v : (Deep a)))) > (struct: (a) Deep ((spine : (Indirect (List a))))) > ;(struct: (a) Deep ((spine : (Deep (List a))))) > > The uncommented version typechecks, but the commented one does not. I > understand why this works in the implementation, but don't know the > theoretical reason why the implementation prevents it, since Indirect > and Deep should be isomorphic. > > On Wed, Apr 10, 2013 at 9:43 PM, Eric Dobson <<a href="mailto:eric.n.dobson@gmail.com">eric.n.dobson@gmail.com</a>> wrote: >> Quick answer is to replace >> (define-type (Fingertree a) (U Empty (Single a) (Deep a))) >> With >> (struct: (a) Fingertree ((v : (U Empty (Single a) (Deep a))))) >> >> Still looking into understanding what is going on, but I believe you >> will need to introduce a Rec somewhere to get it how you want. >> >> On Wed, Apr 10, 2013 at 6:27 PM, Anthony Carrico <<a href="mailto:acarrico@memebeam.org">acarrico@memebeam.org</a>> wrote: >>> I've been reading about fingertrees, and I figure the best way to >>> understand is to implement. This is my first experience with typed >>> racket. Are nested datatypes supported? >>> >>> This is my first try: >>> >>> typed-fingertree.rkt:19:48: Type Checker: Structure type constructor >>> Deep applied to non-regular arguments ((U (Node2 a) (Node3 a))) >>> >>> #lang typed/racket >>> >>> (struct: (a) Digit1 ((v0 : a))) >>> (struct: (a) Digit2 ((v0 : a) (v1 : a))) >>> (struct: (a) Digit3 ((v0 : a) (v1 : a) (v2 : a))) >>> (struct: (a) Digit4 ((v0 : a) (v1 : a) (v2 : a) (v3 : a))) >>> (define-type (Digit a) (U (Digit1 a) (Digit2 a) (Digit3 a) (Digit4 a))) >>> >>> (struct: (a) Node2 ((v0 : a) (v1 : a))) >>> (struct: (a) Node3 ((v0 : a) (v1 : a) (v2 : a))) >>> (define-type (Node a) (U (Node2 a) (Node3 a))) >>> >>> (struct: Empty ()) >>> (struct: (a) Single ((v : a))) >>> (struct: (a) Deep ((left : (Digit a)) >>> (spine : (Fingertree (Node a))) >>> (right : (Digit a)))) >>> >>> (define-type (Fingertree a) (U Empty (Single a) (Deep a))) >>> >>> Thank you! >>> >>> -- >>> Anthony Carrico >>> >>> >>> ____________________ >>> Racket Users list: >>> <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a> >>> > ____________________ > Racket Users list: > <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a> ____________________ Racket Users list: <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a> </blockquote></div>