This comes under the heading of random thoughts rather than active
plans.
We are experiencing a certain kind of constraint creep: the number of
built-in constraints is rising. This suggests an expressive deficiency.
My first itchy feeling that something was wrong came when Swaroop told
me that he needed both copy-compat and top-copy-compat in his formal
type system. Then I started thinking about expressing things like
(deep-const 'a), and realizing that this shouldn't have to be primitive.
The following initially made sense to me as "foundational" type
constraints
[*] (IntLit 'a) and (FloatLit 'a), because they reflect a type
unification that is inherent in the language syntax.
[*] (RefType 'a), for the same reason
[*] (top-copy-compat 'a 'b) because the language cannot
currently express both MUTABLE and CONST as type constraints.
There is also a constraint that we do not currently have, but which
would make sense, and which exists implicitly in Standard ML:
(has-field 'a id) ;; type 'a is a structure type having
a field whose name is /id/
What is starting to disturb me is that HAS-FIELD is somehow more
primitive than IntLit, FloatLit, RefType, or top-copy-compat, and we
don't actually *have* HAS-FIELD. Conversely, if we had the proper
compositional primitives for constraints, none of IntLit, FloatLit,
RefType, or (top-copy-compat 'a 'b) would would need to be primitive.
I provisionally believe that the only ground type constraints should be:
(unifies 'a 'b)
(has-field 'a id)
Other type constraints should be constructed by the following means:
By construction through DEFTYPECLASS
By conjunction, which can already be handled through DEFTYPECLASS:
(C1 'a) if (C2 'a) AND (C3 'a)
By disjunction, as in:
(C1 'a) if (C2 'a) OR (C3 'a)
By structural decomposition, which is a form of conjunction over
syntax:
(C1 'a) if (for-all-fields 'a id:'field
(constraint 'field))
note that in at-all-fields, 'a should be unifiable with any type,
[including union types, meaning all fields in all legs]
and id and 'field are variables that are bound in sequence to each
field type (if any exist). If you prefer, think of "at-all-fields"
as providing a form of macro expansion.
If we have these, then we have:
(forall ((OR (unifies 'a int8)
(unifies 'a int16)
...
(unifies 'a uint64)))
(deftypeclass (IntLit 'a)))
(forall ((OR (unifies 'a (ref 'b))
(unifies 'a (vector 'b))))
(deftypeclass RefType 'a))
(forall ((OR (unifies 'a 'b)
(unifies 'a (mutable 'b))))
(deftypeclass (top-copy-compat 'a 'b)))
;; This is not quite right, because it does not get the field
;; correspondence quite right. We may need some sort of
;; (at-corresponding-fields id 'a 'b)
(forall ((top-copy-compat 'a 'b)
(at-all-fields 'a id:'field
(has-field 'b id:'c)
(copy-compat 'b 'c)))
(deftypeclass (copy-compat 'a 'b))
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
