On Mon, May 4, 2015 at 3:24 AM, Keean Schupke <[email protected]> wrote: > On 4 May 2015 at 00:23, Matt Oliveri <[email protected]> wrote: >> >> > In the type inference systems I have written, you need a ground type for >> > all >> > type variables to allow the program to compile. The only exception is >> > existentials, where you pass the witness at runtime. This is not some >> > coincidence but a fundamental property, and precisely why you need a >> > witness at runtime for existentials but not for any other type. >> >> Hmm, well maybe that's a way to look at it. But it sure doesn't sound >> like the usual way to look at it. > > Its how most real type checkers are implemented, although its different from > the academic descriptions using substitution. Its how the OCaml type checker > is implemented for example. Maybe these other implementers have not realised > that all (non existential) type variables must be grounded, but it is a > requirement, and I am sure I am not the first to spot it.
If you are really sure, then you can provide a reference. I'd like to learn this point of view. But I'm also worried you're just saying something obvious in unfamiliar terms, like that you can't specialize based on types that can't be resolved before runtime. > Polymorphic recursion is tricky, but it has many properties in common with > existential types, in that the 'polymorphic' type cannot be returned and > cannot escape from the closure created by the polymorphically recursive > function. You can see the similarity in the type signatures too: > > data Box a = forall a . Show a => Box a Perhaps this was supposed to be: data Box = forall a . Show a => Box ? > f :: forall a . Show a => a -> Int -> String > > You could look at this another way, after completing type inference, any > ungrounded type variables are existential, or part of polymorphic recursion. > They tell you exactly where you need runtime polymorphism. I like this point of view much better. I mean, it makes your claim above that all non existential type variables must be grounded into a tautology. But for the purpose of this discussion, this seems like the best way for me to understand your possibly-wrong idea of existential. But what's the runtime witness you're saying existentials have? Dictionaries? >> Well, we've established that you're thinking about type systems in a >> very strange way. We'll see how you'd express this after you realize >> you're supposed to be doing type checking at abstract types. > > I don't get your point, I am type checking with abstract types. I am saying > the property of all variables being grounded is there even if you do check > with abstract types. Just because you can't see the elephant in the room, > does not mean it is not there. It's looking now like it _was_ a misundestanding, and you do understand abstract types. You just have this funny habit of classifying all types as either grounded or existential. At least, that's how it appears. The problem of thinking about grounded vs. existential is that it's not something you can determine, looking at a given piece of code. It's a property of the whole program. So it's not something that a source language type system is technically concerned with; it's an implementation issue. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
