On Fri, Jul 30, 2021 at 03:32:54PM -0700, Sorawee Porncharoenwase wrote:
>> When I've had this situation, as a workaround, I've just made a
>> function that returns a fresh-type-variable with all of the supported
>> base types and maybe some constructed types. It's... not great.
>My question is, say, I want to disallow a function, a list of functions,
>list of list of functions, a list of list of list of functions, and so
>Of course, I can express things positively: it's an int or bool or
>listof... what? A list of fresh-type-variable runs a risk of choosing
>function type. So I could do a listof (int or bool or listof ...) for
>another level, and keep increasing levels. Is this what you have in mind?
Yeah, that's the problem with it. You can realistically only specify
a small set of the infinite set of constructible types (granted in
practice the set of types usable by xsmith is bounded as well since it
bounds the tree depth of constructed types). But specifying that list
is a chore and you probably get poor performance if you actually try
to generate many combinations with constructed types. So in practice
when I have this situation so far I just... don't generate as many
things as I otherwise could.
>> However, that feature just hasn't made it to the top of my priorities
>> yet... Sorry :(
>No worries at all! If there's anything that I can help regarding this
>feature, let me know. It looks like the representation of a type right
>consists of a lower bound and an upper bound, and probably this feature
>will require changing the representation, correct?
The upper and lower bounds are about subtyping. If a type changes
through unification it can affect the types connected as upper/lower
bounds. This feature shouldn't change that, other than being more
information that will be conveyed to the related type variables. When
a variable is constrained by unification to remove a type from its
allowed list, all related types in its upper/lower bounds lists also
remove that type. Eg. if variable A is (or string int (-> int int))
and variable B is (or (subtype-of string) (subtype-of int) (subtype-of
(-> int int))) and variable A is constrained to definitely not be a
function, variable B could no longer be a function and still be a
subtype of A. If two variables are unified with `unify!` instead of
`subtype-unify!` (or equivalently by being `subtype-unify!`ed in both
directions) they are more or less merged into a single variable. (IE
the object that you get from `fresh-type-variable` can be merged with
others and they are always canonicalized before doing anything to
Right now a type variable has a list of possible types (or #f for
unconstrained). The list can have any number of base types and every
compound type, but it's limited in that it can only have one of each
compound type (though each compound type may have type variables
inside and thus represent potentially many types).
I think the needed change would be to add a list of disallowed types.
I think this list should probably be applied recursively -- IE it
should be pushed to child types. So eg. if you disallow function
types in a type variable it also disallows lists of functions, etc.
I'm not certain if there are exceptions, though. Would it make sense
to have a recursive and non-recursive version of this?
At any rate, when checking if things `can-unify?`, you would use the
disallowed list as well as the allowed list of both variables to
determine the outcome. When variables are unified, they need to
propagate their disallowed list to related type variables (IE the ones
in the upper/lower bounds lists).
Another thing that would need to be worked out is what exactly to
store in the disallowed list. Constructors for compound types? Or
maybe predicates? Probably base types and predicates is my guess.
At any rate, since we keep emailing about the issue I've thought
through more of it than before, so now I'm much more likely to
actually sit down and do it soon. :P