[Haskell-cafe] Issues(Bugs?) with GHC Type Families

[Ryan Ingram]

On Thu, Mar 6, 2008 at 7:16 PM, Luke Palmer <lrpalmer at gmail.com> wrote:
>  I agree that this would be nice.  But I think that the situation is
>  stickier than it looks on the surface.  Consider this:
>
>     instances GShow [a] where
>         instance [Char] where gShow = id
>         instance [a] where gShow x = "list(" ++ length x ++ ")"
>
>     gShow' :: [a] -> String
>     gShow' = gShow

I'm not so sure.  It's not that hard to imagine a compiler where the
core-language expansion of this code looks like this:

data GShowDict a = GShowDict { gShow :: a -> String }

id :: (a :: *) -> a -> a
id A a = a

length :: (a :: *) -> [a] -> Int
-- definition elided

gShow' :: (a :: *) -> [a] -> String
gShow' A = gShow (mkDict_GShow_List A)

mkDict_GShow_List :: (a :: *) -> GShowDict [a]
mkDict_GShow_List A =
   typecase A of
       Char -> GShowDict (id [A])
       _ -> GShowDict (\xs -> length A xs)

Now, it's true that this means that you can no longer do full type
erasure, but I'm not convinced of the importance of that anyways; if
you look at mainstream languages you generally only get type erasure
for a restricted subset of the types and that's good enough for
performance:
   1) In Java, you only get type erasure for primitive types;
everything else needs its type tag so it can be safely downcasted from
Object.
   2) In C++ only primitive types and structs/classes with no virtual
functions get type erasure; if a class has virtual functions its
virtual function table is implicitly a "type tag".

I don't think the cost is that great; the compiler can easily flag
polymorphic functions that require type information for some or all
arguments and in many cases the type evidence can be passed
"just-in-time" when calling from a non-polymorphic function into a
polymorphic function.

>  When we get to more complex examples like the one you gave
>  above involving constraints, in order to solve for the constraints
>  needed for an instance of C [a] you need a *disjunction* constraint,
>  which vastly increases the likelihood of an undecidable solution.

This is definitely an issue.  I don't have a full understanding of the
methods used for typechecking/inference of typeclasses; I'm just a
programmer who wants MORE POWER :)

  -- ryan