mndrix/mavis

implement types as constraints?

Opened this issue · 0 comments

Consider implementing types as a multifile predicate mavis:has_type/2 which behaves similar to error:has_type/2 but checks the type by adding constraints to a variable. This should allow one to iterate all possible values of a type (in many cases) or to find example values that meet the constraints.

This approach could be useful with union and intersection types as generated by success typing and type inference. After all the constraints are in place, we can determine which values are still valid and report those to the user.

It seems like this would also be helpful for determinism checking. For example, we could generate errors like this: "foo/2 is declared det but can fail with foo(_,alpha)"

I'd like to have more concrete examples of exactly how this will be useful before developing it.