I agree this is too bad. But I'm sorry to say that I'm not going to
improve this right now. It would require fairly major work in the
type unification machinery. The workaround is maybe not the best, but
it's at least pretty easy to do.
On Mon, Aug 23, 2021 at 12:12:38AM -0700, Sorawee Porncharoenwase wrote:
>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.,
> (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,
>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
>On Fri, Jul 30, 2021 at 5:35 PM Sorawee Porncharoenwase <
>> As always, thanks! :)
>> On Fri, Jul 30, 2021 at 5:29 PM William G Hatch <email@example.com>
>>> On Fri, Jul 30, 2021 at 03:32:54PM -0700, Sorawee Porncharoenwase
>>> >> 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
>>> >> base types and maybe some constructed types. It's... not great.
>>> >My question is, say, I want to disallow a function, a list of
>>> >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
>>> 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
>>> >> 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
>>> >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