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