[xsmith-dev] XSmith questions

[Sorawee Porncharoenwase]

As always, thanks! :)

On Fri, Jul 30, 2021 at 5:29 PM William G Hatch <william at hatch.uno> wrote:

> 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, a
> >list of list of functions, a list of list of list of functions, and so on.
> >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 now
> >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
> them.)
>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </listarchives/xsmith-dev/attachments/20210730/0cf13986/attachment.html>