On Sun, May 3, 2015 at 12:12 PM, Keean Schupke <[email protected]> wrote: > Perhaps I should add a little explanation. > > f :: Show a => a -> IO () > f x = putStrLn (show x) > > Although we don't know the type of a when we define 'f' (all we know is that > there must be an instance of show for 'a' which gives us the type > information for checking the definition if f), at some point we use 'f': > > g :: IO () > g = f "test" > > When we do this we polyinstantiate the type of f, and unify 'a' in the > instance of f's polymorphic type with String. This enables us to statically > (at compile time) specialise 'f' for String.
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. > With an implicit argument, 'g' might be called from somewhere that has a > different instance of Show String in scope, meaning we cannot statically > specialise. 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 modules and dependent types have the same problem, but I would be > happy to be proved wrong, as dependent types seem to make a lot of things > simpler. 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. The good news is that adding explicit staging can return control over specialization to the programmer in any case. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
