On Thu, Jul 3, 2014 at 10:25 AM, Jonathan S. Shapiro <[email protected]> wrote:
> On Wed, Jul 2, 2014 at 6:31 PM, Geoffrey Irving <[email protected]> wrote:
>>
>> Languages with typical polymorphism have values that are all the same
>> shape in that sense, typically just a pointer.
>
>
> Not necessarily. BitC and C# stand out as counter-examples, because both
> have explicitly unboxed types, and you can use those types as type
> parameters.
Sorry, by "typical" I sloppily meant languages where that isn't the case. :)
> What is true is that all of the sizes and offsets are known at static
> compile time. That ceases to be true with dependent types, even in the
> constrained virulence that I am contemplating. Given "constructions over
> literals", you could well see a procedure like:
>
> fun f(i: Nat, vec : 'a[i])
>
> where you do not know the size of /vec/ at compile time, but you know that
> the size will be fixed and that you will have it available at link time. It
> raises interesting problems for placement of objects on heap v. stack, and
> it changes how you think about sizeof(). sizeof('a[]) is an error.
> sizeof('a[i:Nat]) is well-typed, but not computable until all types are
> bound. The interesting question is whether we allow cases where we really
> won't know /i/ until runtime, either because we want to take that step or
> merely because we want to compile for code reuse (in which case we may need
> to generalize the implementation of /fun/).
If you're okay delaying such calculations until link time, I'd argue
that the cleanest way is to have full dependent types with the runtime
/ compile time striation added as an extra constraint. This means (1)
all the theory works, (2) everything is fast once you get to the final
compile step (even that is "link" time), and maybe most importantly
(3) the language and grammar are extensible to full dependent types
with runtime and compile time mixed if someone wants to implement that
later on.
I don't think adding this striation to a dependent type system is
particularly difficult: there's usually a different kind of striation
already in place due to universe levels, and from various accounts
that I've seen this poses only mild difficulties. Indeed, if we went
this route, the system would probably be strictly simpler than full
support for universes. We would likely not want a compile time system
that is strongly normalizing, which means we have to essentially run
the compile time portion of the evaluation in a checked interpreter,
which means we don't need to worry about Girard's paradox, which means
Type : Type is fine.
I realize the above may be outside the scope of bitc, and certainly
requires compilation to become undecidable in the sense of "easy but
nonterminating". I personally don't think this is a problem, but we
seem to differ on this point. :)
As a compromise though, if you're concerned about future extensibility
to full dependent types, we definitely want to have the same grammar
for types and terms. I've written a prototype interpreter with
otherwise Haskell-like syntax where this is the case, and if I recall
correctly the only problem was the ambiguity of
let f x = y
In the language I was writing there was no grammar separation between
constructors and variable names, so unlike Haskell there was an
ambiguity between defining a function and pattern matching on a
constraint. Though now that I write this it doesn't seem to be
related to terms vs. types at all, so maybe there isn't a problem. I
can look up how we worked around the ambiguity if you're curious,
since I don't remember the resolution offhand.
>> At least an earlier version of bitc did template-like instantiation to
>> push the problem to compile time. I do not remember whether that's changed.
>
> Conceptually it hasn't changed, and it can't because of unboxed types. There
> are various points in the continuum between unit-of-compilation time and run
> time where that expansion can occur. The hard requirement is that it can be
> checked early, and that it be possible to pre-expand everything in the
> absence of dynamically introduced types (e.g. through dynamic loading). So,
> for example, I don't want to have to put a run-time code generator into an
> operating system kernel.
Great.
Geoffrey
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
