[racket] fingertree / nested datatype
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