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. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
