[racket] fingertree / nested datatype

The restriction is supposed to be that a type constructor T a = ...
can't have some field in the ... that's a use of T other than to apply
it to a.

Unfortunately, this restriction (and all the other literature on this)
is presented for ML-like languages, which have neither structs like
TR, nor union types, nor subtyping.  That's why we haven't been able
to easily transfer the literature on how to add non-regular data
types, and why I seem to have implemented an insufficiently-strong
restriction.

So I think we need to think harder about this, but I don't have a
great suggestion for fixing it at the moment.

Anthony, for your use, you can probably use the encoding technique
described in the paper I linked to about data structures in TR.

Sam

On Sat, Apr 13, 2013 at 3:23 AM, Eric Dobson <eric.n.dobson at gmail.com> wrote:
> I believe this is the issue that the the check is trying to prevent.
>
> Sam, can you explain how the indirection is supposed to solve this?
>
> What is currently happening is we ask:
> (subtype (Deep Number) (Deep Any)), which computes
> (subtype (Indirect (List Number)) (Indirect (List Any))), which then computes
> (subtype (Deep (List Number)) (Deep (List Any))), and then repeats.
>
> On Fri, Apr 12, 2013 at 5:40 PM, Anthony Carrico <acarrico at memebeam.org> wrote:
>> On 04/11/2013 08:51 AM, Sam Tobin-Hochstadt wrote:
>>> Yes, an explicit struct involves an explicit indirection, and thus
>>> produces a regular tree.
>>
>> Using Eric's example:
>>
>> #lang typed/racket
>>
>> (struct: (a) Indirect ((v : (Deep a))))
>> (struct: (a) Deep ((spine : (Indirect (List a)))))
>> ;(struct: (a) Deep ((spine : (Deep (List a)))))
>>
>> This checks fine, but try to use it:
>>
>> (: test ((Deep Number) -> Boolean))
>> (define (test ft) (Deep? ft))
>>
>> And it hangs. So maybe indirection just pushes the problem somewhere else?
>>
>> --
>> Anthony Carrico
>>
>>
>> ____________________
>>   Racket Users list:
>>   http://lists.racket-lang.org/users
>>