[xsmith-dev] XSmith questions

[Sorawee Porncharoenwase]

I want to express a type constraint that it’s either a product type of
length 0, 2, or 3. Is there a way to do that? fresh-type-variable with
arguments seems like a solution, except that the composite type isn’t
allowed to be repeated. Usually, if I have a generic type of the same
arity, I can simply push fresh-type-variable in. E.g.,

(fresh-type-variable
 (immutable (array-type ...))
 (immutable (set-type ...)))

=>

(immutable (fresh-type-variable (array-type ...) (set-type ...)))

The problem is that product-type‘s argument is a list of types of false, so
fresh-type-variable doesn’t work there.

I guess I can create generic types product0, product2, and product3, and
put them in fresh-type-variable, but well, I really want to avoid doing
this.












On Fri, Jul 30, 2021 at 5:35 PM Sorawee Porncharoenwase <
sorawee.pwase at gmail.com> wrote:

> 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/20210823/18b7adc2/attachment.html>