> 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. _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
