TypeFamilies vs. FunctionalDependencies & type-level recursion

[oleg at okmij.org]

> One question I have is why you need UndecidableInstances.  If we got
> rid of the coverage condition, would your code be able to work without
> relying on contexts for instance selection?

UndecidableInstances is the name for a conglomerate of various
relaxations -- the fact that causes discord since we may agree
about some relaxations and disagree about the others. 

One can see that all type functions (except the general Apply) are in
fact terminating. For example, the termination of TREPEQ and TREPEQL
can be seen by structural induction. However, since these two
functions are mutually recursive, a termination checker, in my
experience, will likely to have hard time seeing that. Let alone GHC
(which isn't a termination checker to start with). In short, I need
UndecidableInstances since GHC will not accept code without the flag
since it can't see type functions terminating.

> If you were to implement this in GHC you would encode the TC_code as
> the packge, module, and type name, letter by letter?  (Or bit by bit
> since symbols can contain unicode?)

Indeed. It crossed my mind to make a joke that GHC ought to best SML
by lifting the whole Unicode to the type level.

> How would you make this safe for dynamic loading?  Would you have to
> keep track of all the package/module names that have been linked into
> the program and/or loaded, and not allow duplicates?  Is dynamic
> unloading of code ever possible?  Or at least is re-loading possible,
> since that appears to be key for debugging web servers and such?

I must read up on Andreas Rossberg's work and check AliceML (which is,
alas, no longer developed) to answer the questions on safe dynamic
loading. AliceML is probably the most ambitious system to support
type-safe loading. See, for example

http://www.mpi-sws.org/~rossberg/papers/Rossberg%20-%20The%20Missing%20Link.pdf

and other papers on his web page. He now works at Google, btw.


One comment about unloading: we've `dealt' with that issue in
MetaOCaml by not doing anything about it, letting the garbage code
accumulate. It is hard to know when all the code pointers to a DLL
are gone. GC do not usually track code pointers. One has to modify GC,
which is quite an undertaking. I suppose one may hack around by
registering each (potential) entry point as a ForeignPointer, 
and do reference counting in a finalizer. Since a DLL may produce lots
of closures, each code pointer in those closures should be counted as
an entry point. 

> Finally, how do you express constraints in contexts using type
> families?  For example, say I wanted to implement folds over tuples.
> With fundeps (and undecidable instances, etc.), I would use a proxy
> type of class Function2 to represent the function:

Your code can be re-written to use type functions almost mechanically
(the method definitions stay the same -- modulo uncurrying, which I used
for generality). I admit there is a bit of repetition (repeating the
instance head). Perhaps a better syntax could be found.


{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module PolyShow where

-- Higher-order type-level functions

class Apply f a where
    type ApplyR f a :: *
    apply :: f -> a -> ApplyR f a


-- An example, to show something of class Show and put the result in
-- a list endo:
data PolyShows = PolyShows

instance (Show a)
    => Apply PolyShows ([[Char]] -> [[Char]], a) where
    type ApplyR PolyShows ([[Char]] -> [[Char]], a) = [[Char]] -> [[Char]]
    apply _ (start,a) = start . (show a :)


-- Define a class for folds, as well as an instance for each tuple size:

class TupleFoldl f z t where
    type TupleFoldlR f z t
    tupleFoldl :: f -> z -> t -> TupleFoldlR f z t

instance TupleFoldl f z () where
    type TupleFoldlR f z () = z
    tupleFoldl _ z _ = z
instance (Apply f (ApplyR f (z, v0), v1), Apply f (z, v0))
    => TupleFoldl f z (v0,v1) where
    type TupleFoldlR f z (v0,v1) = ApplyR f (ApplyR f (z,v0),v1)
    tupleFoldl f z (v0,v1) = apply f ((apply f (z,v0)), v1)


test = tupleFoldl PolyShows (id::[String]->[String]) (1,2) []
-- ["1","2"]


And here is a bonus

data PolyShows' = PolyShows'

instance (Show a, t ~ ([String] -> [String]))
    => Apply PolyShows' (t, a) where
    type ApplyR PolyShows' (t, a) = [[Char]] -> [[Char]]
    apply _ (start,a) = start . (show a :)

test' = tupleFoldl PolyShows' id (1,2) []
-- ["1","2"]


The type annotation on id is no longer needed.


> With fundeps and undecidable instances, if I use the default context
> stack depth of 21, my left and right folds crap out at 10 and 13
> element tuples, respectively.

When I generate my web pages with HSXML, I set the context depth to 180.