the MPTC Dilemma (please solve)

[Bulat Ziganshin]

Hello Lennart,

Sunday, March 19, 2006, 4:05:03 AM, you wrote:

LA> I have to agree with Manuel.  I write a lot of Haskell code.
LA> People even pay me to do it.  I usually stay with Haskell-98,

when i wrote application code, i also don't used extensions very much,
i even don't used Haskell-98 very much and afair don't defined any type
classes at all

but when i gone to writing libraries, that can be used by everyone,
type classes and requirement in even more extensions is what i need
permanently. in particular, i try to write library so what any
conception (stream, Binary, reference, array) can be used in any monad
and that immediately leads me to using MPTC+FD. moreover, problems with
resolving class overloading and other deficiencies of current
unofficial Hugs/GHC standard are permanently strikes me

so, from my point of view, we should leave MPTC+FD+any well-specified
extensions in resolution of overlapping classes. but these should be
seen only as shortcuts for the new type-calculation functions, like
the old-style "data" definitions now seen as shortcuts for GADT ones

just some examples how this can look:

i had a class which defines "default" reference type for monads:

class Ref m r | m->r where
  newRef :: a -> m (r a)
  readRef :: r a -> m a
  writeRef :: r a -> a -> m ()

instance Ref IO IORef where ...
instance Ref (ST s) (STRef s) where ...


this class allows to write monad-independent code, for example:

doit = do x <- newRef 0
          a <- readRef x
          writeRef x (a+1)
          readRef x

can be runned in IO or ST monads, or in any monad derived from IO/ST
(with appropriate instance Ref definitions). As you can see, even such
small example require using FDs.



That's all great but not flexible. That we required is a real
functions on type values. In ideal, types should become first-time
values, compile-type computations should be allowed (what resembles
me Template Haskell), and computed types should be allowed to
used in any place where current Haskell allows type literals.
moreover, runtime-computed types can be used for dynamic/generic
programming, but that is beyond of our current theme.

really, Haskell already has functions on types:

type Id a = a
type Two a = (a,a)

and so on. but these definitions don't have full computational (Turing)
power, can't contain several sentences, can't be split among different
modules/places and so on, so on. on the other side, class definitions
are our most powerful type functions, but has very different syntax and
semantic model compared to plain functions, plus had some additional
duties (declaring a family of functions)



how about adding to type functions the full power of ordinal
functions? first, data/newtype declares new type constructor on its
left part in the same way as it defines new data constructors on its
right part:

data List a = Nil | Cons a (List a)

defines Nil and Cons data constructors and List type constructor.
Together all data constructors defined in program plus primitive types
(Int, Char...) defines a full set of types that can be
constructed/analyzed by type construction functions. so, we should
not only allow to construct new more complex types on the right side of
type function, but also allow to analyze complex types on the left
side of function definition! :

type Element (List a) = a
     Element (Array i e) = e
     Element (UArray i e) | Unboxed e = e

cute? i love it :)  i also used pattern guard here, it's a partial
replacement of Prolog's backtracking mechanism. of course, to match
power of type classes, we should allow to split these definitions
among the whole module and even among the many modules. library
type function should be allowed to be extended in application modules
and application definitions should have a priority over library ones

this will allow to rewrite my Ref class as:

type Ref IO = IORef
     Ref (ST s) = STRef s



Next problem is declaring types (to be exact, kinds) of type
functions. currently, kinds are defined only in terms of arity:

type ReturnInt (m :: * -> *) = m Int

but what we really want is to declare that `m` is Monad here:

type ReturnInt (m :: Monad) = m Int

or

type ReturnInt :: Monad -> *
type ReturnInt m = m Int

i also propose to show kind arity by using just "**", "***" instead of
current "*->*", "*->*->*". the above definition can be extended in
user module by:

type ReturnInt (ST s) = Int

but not with

type ReturnInt Int = IO

because last definition break types for both left and right sides



having all this in mind, we can break class definitions into the
lower-level pieces. say,

class Monad m where
    return      :: a -> m a
    fail        :: String -> m a
instance Monad IO where
    return = returnIO
    fail   = failIO

translates into:

type Monad :: ** -> (a -> m a, String -> m a)
type Monad IO = (returnIO, failIO)

i.e. Monad is function that translates '**' types into the tuple
containing several functions. well, translation is not ideal, but at
least it seems promising

next, my Ref class is a Monad->Reference function (what is established
by FD used), so:

type Ref :: (Monad m, r :: **) => m -> (r, a -> m (r a), r a -> m a, r a -> a -> m ())
type Ref IO = (IORef, newIORef, readIORef, writeIORef)




many MPTC declarations is not functions, but relations. That
makes programmer's life easier, but compilation harder and returns to
us in form of strange compiler behavior and numerous prohibitions. i
suggest see such classes as the types->functions definitions. for
example:

class (HasBounds a, Monad m) => MArray a e m where
    unsafeRead  :: Ix i => a i e -> Int -> m e
    unsafeWrite :: Ix i => a i e -> Int -> e -> m ()
instance MArray IOArray e IO where ...
instance (Unboxed e) => MArray IOUArray e IO where ...

can be translated to:

type MArray :: (HasBounds a, Monad m, e :: *)
    =>  a -> e -> m -> (UnsafeRead a e m, UnsafeWrite a e m)
type UnsafeRead  a e m = Ix i => a i e -> Int -> m e
type UnsafeWrite a e m = Ix i => a i e -> Int -> e -> m ()

type MArray IOArray e IO = (arrRead, arrWrite)
     MArray IOUArray e IO | Unboxed e = (arrReadUnboxed, arrWriteUnboxed)




well, i don't catched all the problems:

1) how these definitions allow us to select proper "instance" for
operations like readRef? i don't know, my examples even don't define
names of functions. well, i can imagine something like this:

type ReadRef (IORef a) (IO a) = readIORef
     ReadRef (STRef s1 a) (ST s2 a) | s1==s2 = readSTRef

what maps types of arguments/result of readRef invocation to proper
function body, but that's too verbose and don't solves the problems
that solves FDs

2) i don't proposed good syntax to rewriting classes in terms of type
functions. i think that using structures with named fields should be
great here and will closely resembles ML's functors


i propose to start with type functions, allow type declarations for
type functions including using classes as "types of types" and allow
to mix types and ordinal values in type functions arguments/results

i don't see any good alternative to using prolog-like relations to
declare classes:

type Ref :: (Monad m, r :: **) =>
  m -> r -> NewRef m r -> ReadRef m r -> WriteRef m r -> ()

type NewRef m r  =  forall a . a -> m (r a)
type ReadRef m r  =  forall a . r a -> m a
type WriteRef m r  =  forall a . r a -> a -> m ()

type Ref IO IORef newIORef readIORef writeIORef = ()
     Ref (ST s) (STRef s) newSTRef readSTRef writeSTRef = ()

but this definition again loses the FD :(



-- 
Best regards,
 Bulat                            mailto:Bulat.Ziganshin at gmail.com