On 3 May 2015 at 22:52, Matt Oliveri <[email protected]> wrote: > > It sounds like you're saying you only check f once it's been > specialized for String. That's more like C++ templates than real type > abstraction. It pins strata to stages, which restricts the type > systems you can handle, and it isn't efficient, since you type check > each specialized instance of f, rather than check f in the abstract > once and for all. >
Its how all type checkers work as far as I understand. An ungrounded type variable is a failure to type check. > Yes, but at this point, I'm more concerned you don't know what type > abstraction is than that you think implicit arguments should be > abandoned for this reason. > I think it would be good if you could explain what you mean by type-abstraction, as I think I am thinking of something slightly different. > Dependent types generally have this problem. Non-first-class modules > alone don't, I think, but combining them with polytypic equality > and/or pretty printing (Eq and Show, essentially) do. > Associated types in modules are effectively dependent types (they are types that depend on values), so ML modules have this problem. > > The good news is that adding explicit staging can return control over > specialization to the programmer in any case. > At the cost of making the program code harder to understand, full of meta-quotation and all sorts of other ugly stuff. Any language with quoting, like MetaML, Template Haskell etc, is not nice to write nor debug. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
