On Sat, Dec 27, 2014 at 1:50 PM, Jonathan S. Shapiro <[email protected]> wrote:
> On Sat, Dec 27, 2014 at 10:20 AM, Matt Oliveri <[email protected]> wrote:
>>
>> Well with an array, there's a non-type-specific meaning for the
>> indexes--they're just unsigned integers.
>
> At the language level type system, what you say is true. At the instruction
> level type system, *both* forms of indices are actually offsets.
>
> Yes, I agree the offsets are type-specific, but that's mainly so that we
> know the type of a[i] without knowing the value of i. And I certainly agree
> from a pragmatic perspective that we would very much like to know that type.
Well, also that you don't want to access the middle of a field,
unaligned. If you can access one record type with another record
type's offset, then (other than some special cases) you've broken the
record abstraction.
> But if restrict ourselves - just for a moment - to literal indices like
> a[2], we would be looking at something much more like a record, because that
> literal tells us explicitly which cell we are looking at, after which
> there's no real reason to require all of the cells to have the same type.
Just to be clear, I was distinguishing "dependent arrays", which have
a particular index type and different elements can have different
types (and sizes), from what I should've called "first-class labels",
which are a candidate index type to use on all dependent arrays that
act like records. I was saying first-class labels are not a good idea
to implement records, and it looks like you agree.
> Assume that tuples are unboxed. If that's the case, then I can form an
> offset for ( 5.6247, "abc" )#2 just as easily as I can form the offset for
> (5.6247, "abc").snd. This is true because the indexing expression is a
> literal, not a variable. That's the kind of thing I'm saying when I talk
> about literal identifiers. Identifiers as actual values is another matter
> entirely.
Ah I see. In that case, it seems fine, but then I don't see what it's
buying you.
>> But copy-and-update does seem like adding environment entries,
>> assuming the type is allowed to change. (I guess I'm not following
>> your train of thought, from copy-and-update to literal identifiers.)
>
> The type only changes if new field names are introduced by the
> copy-and-update operation, or if the type of an existing field name is
> altered (comparable to shadowing with let).
Right, that's the similarity. I was confirming that you could change
the type associated with a name--like shadowing with let--since I
haven't read the F# spec.
> What I'm saying about literal identifiers in the copy-and-update context is
> that when we see something like
>
> (r:'R) with myField = 42.3
>
> we can view the "with" as a polymorphic ternary function:
>
> HasField('R :: Record, 'id :: Ident, 'fieldType) =>
> with: 'R -> 'id -> 'fieldType
Maybe I don't know this notation. Where is the return type?
> in exactly the same way that we can view array indexing as a polymorphoc
> binary function:
>
> forall 'index :: Nat < 'bound :: Nat =>
> arrayLookup: 'a[bound] -> 'index -> 'a
>
> That is: literals can be "lifted" to types and then we can do polymorphism
> over them in the usual way.
>
> And in that (admittedly odd) view of things, an environment is merely a
> function
>
> tyfn 'ident -> 'valueType =>
> env : ('ident :: Ident) -> 'valueType
Well I don't know how to read that either, but I figure this can be
worked out. Really though, if these identifiers are really only
literals, then I don't see how looking at it this way gives any extra
generality. Usually the reason to make an operation into a function is
higher-order programming. But you can't do much with these functions
in a higher-order way, or else the compiler won't be able to treat the
identifiers as literals without inlining a ton of stuff.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
