[racket] fingertree / nested datatype

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.
On Apr 11, 2013 7:23 AM, "Sam Tobin-Hochstadt" <samth at ccs.neu.edu> wrote:

> 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 <eric.n.dobson at gmail.com>
> 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 <eric.n.dobson at gmail.com>
> 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 <acarrico at memebeam.org>
> 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:
> >>>   http://lists.racket-lang.org/users
> >>>
> > ____________________
> >   Racket Users list:
> >   http://lists.racket-lang.org/users
> ____________________
>   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/20130411/8a4aca02/attachment-0001.html>