On Wed, Jul 2, 2014 at 12:19 PM, Geoffrey Irving <[email protected]> wrote:
> On Wed, Jul 2, 2014 at 11:04 AM, Jonathan S. Shapiro <[email protected]> wrote:
>> Thanks, William. The pointer to Idris is really helpful. Their tutorial is
>> kind of interesting, since the sections on dependent types don't actually
>> use dependent types!
>>
>> I have to say that I'm waffling here, for three reasons.
>>
>> First, most of the simple use-cases turn out to involve literals, and we
>> simply don't need dependent type for that. Admitting literals into types
>> goes right up to the edge of true dependent types, but it does not step over
>> the line of turning types into terms. I think it's very clear what the
>> benefit of "literal types" (there's a proper term, but that's what I've been
>> calling them here) into BitC. I also think that's a step that is small
>> enough to be readily explained to programmers - it doesn't require taking a
>> leap into types as terms that will be really jolting to most programmers.
>>
>> The second is probably just my ignorance, but it's not always bad to worry
>> about how what you don't know will bite you. :-) The issue is this: in BitC,
>> types define the shapes of data structures even as they describe the nature
>> of the inhabiting values. I don't know how that relationship really works in
>> dependent type systems. It seems obvious to me that a language with
>> dependent types must ultimately arrive at shapes for all of the values it
>> manipulates, but I'm ignorantly nervous about that part.
>>
>> The third issue is that I have no personal experience with dependent type.
>> While designing a language to support them actually is a really good way to
>> learn them, I'm not so sure that learning language should then be published.
>> :-)
>>
>> What I'm coming to, here, is that I think at this stage I should stick to
>> what I know, which is the literal types part of all this. That's pretty
>> powerfully expressive already, and within the realm of what can be
>> explained.
>
> Assuming you mean literals literally, I don't think they quite cover
> the cases one wants. For example, if you have a static size array
> type parameterized by a size, say Vec n a for n copies of type a, you
> very quickly want to say Vec (n+1) a, and then after that you very
> quickly want to say Vec (sqr n) a, and so. C++ has already gone
> through a lot of evolution on this front, so it'd be good for bitc to
> skip to the end.
>
> The worst thing that C++ got wrong initially was using a different
> syntax for compile time metaprogramming and runtime programming, so
> that we ended up with Vec (mpl::sqr<n>::value) a. If (1) bitc does
> not allow Vec (sqr n) a, and (2) there is *any* way to do
> mpl::sqr<n>::value, people will start to do it, and you live in syntax
> hell for the rest of the lifetime of the language.
>
> C++ has now solved this to some extent with constexpr, but a constexpr
> can't return a tuple. This means that if you want Vec n0 (Vec n1 a),
> and you want the same code to split out both n0 and n1, there's no
> clean way to do it. Bitc could conceivably solve this if you had
> something like constexpr for all purely functional code, but I suspect
> you are (somewhat justifiably) afraid of going this far (though I
> would love it if you did :)). I don't think it is particularly
> difficult to implement: all it requires is knowing which code is
> functional and which isn't, and being able to run an interpreter for
> the functional part at compile time. Certainly it has been done
> before (tik-c does a lot more, for instance).
Self-correction: C++11 constexprs can return tuples and other structs,
but the structs they return must be declared completely separately
from the normal structs (which I only just now learned):
http://en.cppreference.com/w/cpp/concept/LiteralType
I don't really know the reason for this separation, unless it was to
satisfy FUD. The compiler already has to check that constexprs
satisfy constraints, so you could just as easily let normal functions
be used as constexprs as long as they satisfy those same constraints
without forcing the user to annotate.
Geoffrey
> In terms of your worry about shapes, the issue with dependent typing
> is that there is no "now compile time is done" point in a fully
> dependent typed language where you know what n is in Vec n a. That
> is, there is no hard striation between compile time and runtime.
> There is a hard striation between type checking and running, but type
> checking does not tell you what n is, just that whatever it is at
> runtime will be safe. I think a compile vs. runtime striation is
> reasonable for bitc, and don't think it is particularly hard to
> implement.
>
> Geoffrey
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
