There’s a bit of a problem for type-inference. For instance, what is the type
of:
\a . (a[1], a[0])
If a is a vector, say Vector<E>, then the type is Pair<E, E>. If a is a tuple,
say Tuple<A, B, …>, then the type is Pair<B, A>. If a is a pair Pair<A, B>,
then the type is Pair<B, A>.
So, in order to get ahead on this one, you would have to introduce constraints
such as Indexed<N, T> where N stands for a literal number. Then the type would
be:
(V : Indexed<0, A>, V : Indexed<1, B>) => V -> Pair<B, A>
Needless to say, this is a lot of complications and one might argue that it is
simply better to avoid this by having to annotate the type.
PKE
From: [email protected] [mailto:[email protected]] On
Behalf Of Jonathan S. Shapiro
Sent: Thursday, September 04, 2014 11:13 AM
To: Discussions about the BitC language
Subject: [bitc-dev] Heterogeneous vectors
The AST issue also has me thinking about heterogenous arrays and indexing
operations.
First, let's consider tuples. Give a tuple type (char, int, float) we could
very easily adopt indexing notation, as in:
let tup = ('a', 1, 3.414)
in
tup[1] // has 'int' type
Aside from the inconvenience for type inference (we can no longer assume that
[] means vector), there's no obvious problem here. Matters become rapidly more
complicated if the index operation can be performed using a variable, which is
part of why selectors on tuples have tended to use some syntax like "#1" rather
than "[1]".
From a case analysis perspective, we end up with three cases here:
1. Heterogeneous element types combine easily with literal indices
2. Homogeneous element types combine easily with either literal or value
indices
3. Heterogeneous element types can combine with value indices, but only with
some form of dependent type analysis
The reason that a vector has to have homogeneous type is pragmatic. Since we
can't put a bound on it's length, we can't enumerate the types of all elements,
and so we don't really have a way to use literal indices. Conceptually,
however, it isn't hard to imagine a hybrid type in which we say something like
"the first three cells have types 'a, 'b, and 'c, and the remaining (variable
number) of cells have homogeneous type 'd.
In the case of a value (that is: non-literal) index on a heterogeneous sequence
type, we could imagine returning a type-tagged pair if that made the language
feel more sane.
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
