Evan Hanson <ev...@foldling.org> writes:

> Hey megane, good find once again. Sign-off attached.
>
> That's a nice idea regarding tv handling. Some thoughts about that are
> inline below.

Hey Evan, thanks for taking a look.

Sorry, I forgot there was this PS about type variable records in the
mail when I asked you to look at this mail. I did not want to bother you
with that. This is not a pressing issue :) I commented on the matter
more, but feel free to skip that. I am just thinking aloud.

>
> In the meantime, I think the second patch attacheed to this email would
> be good to apply as well. It uses the "real" real name table in a
> similar way to what was done before (this should have been the approach
> used in the first instance, really), which avoids interfering with macro
> handling but still prints the aliases nicely. This avoids a regression
> until something more full-on like what you've described can be done.

There is a fix to this renaming issue in the patch set I just posted.
It is in the last commit (0012).

Maybe we can postpone this fix until that patch set gets resolved?

>
> Cheers,
>
> Evan
>
> On 2018-12-02 18:02, megane wrote:
>> Personally I feel the best way to handle this would be to remove 'forall
>> altogether inside the scrutinizer and use, for example, a record for the
>> typevariables inside the types. For example:
>>
>> (forall (a) (vector a)) would be converted to:
>>
>> `(vector ,(make-type-variable 'a (generate-new-tv-id) #f))
>
> We'd need to include constraints in there somehow, too.

True. Like this: (make-type-variable 'a (generate-new-tv-id) #f #f).
>
> The "forall" representation has the benefit of making it possible to
> know what type variables appear in a form without walking it again (once
> the type has been constructed) since they can be coalesced onto the
> root. I'm not sure how much we take advantage of that currently, so it
> might not matter, but there may be a performance cost if we lose that
> property.

I think the biggest benefit for the forall style is the explicitness.
Especially when printing. It shows which symbols are type variables, and
what their constraint types are. I think this style has its uses even if
the internal representation changes.

I think the biggest cost from typeenv comes from the two first tests in
'match1. Here we check all symbols against the typeenv, which is a
linear search. If we use records, it's just one test.

>
> Regardless of the representation used within the scrutiniser, It would
> be nice to use the quoted shorthand when printing typevars, now that we
> have it.

This is handled in the pp patchset I mentioned above.

>
>> This way we could get rid of the typeenv too.
>
> How so? Wouldn't we still need to pass the "active" typeenv around to
> resolve/match-types/etc. same as today?

When using tv records the typeenv would exist implicitly in the records
contained in a type.

The typeenv is the mapping from tv-name to a list (tv-name
false-or-unified-type false-or-constraint). When using tv records the
information in this list would exists directly in the tv record. We
don't need to look it up from anywhere.

So today, we have a type (forall (a b) (procedure (a) b)). From this we extract
the typeenv ((a #f #f) (b #f #f)), which we would pass to match-types.

With tv records you would convert the type to
(procedure (,(make-tv 'a (gen) #f #f)) ,(make-tv 'b (gen) #f #f)), which you can
pass to match-types.

In match types, instead of checking the typeenv, you just test (tv? t).

>
>> The unification trail would have to be changed too. Turns out it's
>> enough to just push the type-variable record to the trail. When undoing
>> the unifications just grab a record from the trail and set the type to
>> #f.

I'll try to expand this a bit.

The trail is used to record unifications. Today, when a unification
happens in 'match1, the unified variable's name symbol is added as the
head of the 'trail global.

To undo unifications, we take a symbol from the trail. Lookup the tv's
list , as described above, from a relevant typeenv. Then we set the
second element of that list (the false-or-unified-type part) back to #f.

When using tv records we just grab a tv record from the trail and set
the type field back to #f.

_______________________________________________
Chicken-hackers mailing list
Chicken-hackers@nongnu.org
https://lists.nongnu.org/mailman/listinfo/chicken-hackers

Reply via email to