On Wed, Jul 2, 2014 at 2:04 PM, Jonathan S. Shapiro <[email protected]> wrote: > Admitting literals into types ... 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 defining characteristic of dependent type systems is not types as terms, but type checking depending on the execution of terms. Clearly literal types avoids both, but even true dependent type systems do not need to be able to use types as terms. That's a consequence of universe types. > 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. Are you talking about Church vs. Curry-style typing? Virtually all dependent type systems are Church style, so the type strongly dictates how values can be constructed. (Perhaps too strongly.) > 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. > :-) I would advise that you do some hacking in at least one existing dependently-typed language before trying to design your own. There's a surprising pile of new subtleties once you take dependent types seriously. > 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. Literally just literals though? What about variables? Basically the trouble only comes in once you start needing a theory of equality for values. (To get a theory of equality for dependent types.) _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
