On Tue, Jun 16, 2015 at 4:10 PM, Matt Oliveri <[email protected]> wrote: > On Tue, Jun 16, 2015 at 5:43 PM, Matt Rice <[email protected]> wrote: >> On Tue, Jun 16, 2015 at 1:06 PM, Matt Oliveri <[email protected]> wrote: >>> On Tue, Jun 16, 2015 at 7:05 AM, Matt Rice <[email protected]> wrote: >> >> (reordering a bit to reply to both these things below) >> >>>> and frustratingly set >>>> up so that you cannot speak about type's return value, or specify some >>>> return values future type existentially, >>> >>> I don't understand. A type doesn't have a return value. And what is a >>> "future type"? You're not talking about futures, are you? >> >> In a sense yes, parsers and languages are *full* of stuff which will >> only be representable in the future. > > I mean this "futures": > http://en.wikipedia.org/wiki/Futures_and_promises
I mean pretty much existential type, except that it's equivalent to a value. >> value:type is one of these things, > > I think you're being _too_ creative here. The typing judgement is just > some metalanguage syntax. I don't see how it could be something whose > execution involve futures, or any side effects. It's unconventional to > even think of it as being executable. In general it is the metalanguage that I have a problem with, its goal is to confine types and their values to the meta language in which they will used equivalently across the entire program. let me restate that, I have a problem when the meta language results in the loss of the type as it would be represented by a value... This is what I meant when I was trying to say you lose the paradigm by 'going down an order', unless that meta-language is pure and evaluates to another language which retains types as values, you can not get the values back out of the meta-language, my argument is that there are better ways to do confinement, and by its nature it leads to a more expressive system that can be as unexpressive as you desire... being able to do futures and stuff is just a biproduct of working with values (functions that accept types as parameter, and return types as return values). Which implies that the phase distinction is muddied... I just don't see the point of adding on meta-languages *if* we can express them in a unified core language. >> so we collect all the arguments *before* we can solve whatever >> it is we are trying prove, it is useful if everything is consistent >> across phases. > > A thing to prove is a statement. It's syntax. You don't need to > evaluate anything. So I don't see how we'd be waiting on futures in > "value:type". The types are *input* to the compiler, the resulting AST type is generally input to the parser... >>>> its easy to fall under the spell of omniscient type values, rather >>>> than isolating phases from one another, and reusing the language. >>> >>> I don't know what you mean by "omniscient". But it kind of sounds like >>> you're against having code be reusable across phases. >> >> That is my main problem with type, is exactly that it doesn't have a >> return value, > > If by return value, you mean the result of evaluating an expression, > then type expressions _can_ have a return value: a type > representation. But most dependent type systems don't allow you to > inspect a type representation (e.g. with a type case), so they might > get optimized out before runtime. Or they might be used internally to > implement polymorphism. > >> the low-level sequence is value:type = sequence_of_one_or_more_things, >> so there is a 1 < - n, (one type for every typed sequence), >> further there is a 1 -> n fields to a type (or we can go from 1 type, >> to n typed values), > > I'm not sure, are you talking about reduction sequences, from > operational semantics? Otherwise I have no idea. > >> this expansion and contraction, is rather fundamental, and so saying >> that type doesn't have a return value is implying type is global and >> ambient, because it needs to be globally consistent, I believe there >> are other ways of proving global consistentcy, through isolation and >> the interpretation of the types value... > > I don't know what you mean by global consistency. And I'm still not > sure I know what you mean about whether a type has a return value. > >> this *allows* types to be >> reusable across phases, > > Types are already reusable across phases. In a dependent type system, > all computations are constrained by the same type system, whether they > take place at compile time or runtime. > >> if we take away the "return value" of 'type', >> when we absolutely *remove* the ability to pass them as arguments and >> use parameter passing as a mechanism for giving or denying authority >> to types, so the easiest analogy I can come up with is that an >> ambient/global idea of type, essentially builds a fence, where it >> seems reasonable that a wall would suffice, > > I don't see why you're talking about authority, since type expressions > need to be pure computations. > >> you'll most certainly have to drop subtyping though, or at move to its >> equivalent in the space where types are values... > > Subtyping still makes sense when types are passed around in the same > way as values. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
