On Tue, May 31, 2011 at 1:40 AM, Patrick Browne <patrick.browne@dit.ie> wrote:
Continuing the thread on model expansion.
I have changed the example trying to focus on expanding models of M in G
Why is the operation ! ok or RHS but not visible on LHS of G?
The equation itself does not seem to suffer from the dependent type
problem of my previous post.

class M a where
 (!)  ::  a -> a -> a
 e :: a


class M a => G a where
 (!-)  ::  a -> a -> a
-- OK in G
 a !- e = e ! a

This doesn't do what you think.  This is equivalent to

(!-) = (\a e -> e ! a)

That is, "e" is lambda-bound here, not the same "e" from M.  In this case you've defined (!-) as "flip (!)"

When you define functions in a class declaration, you are just defining a default implementation.  Generally this is used when you can implement some functions in terms of the others, such as:

class Eq a where
   (==) :: a -> a -> a
   (/=) :: a -> a -> a

   a == b = not (a /= b)
   a /= b = not (a == b)

Now someone making an instance of this class need only define (==) or (/=); the other one will be defined via the default instance.  (This has the somewhat undesirable property that 'instance Eq X where' with no methods is a valid instance declaration but in that instance == and /= are infinite loops)

Maybe this will help you think about this: what code do you expect to write for instances of this class?

instance M Int where
  e = 0
  (!) = +

instance G Int where
  -- do I need to write any code here?

It seems to me you are expecting the compiler to automatically derive the definition 'inverse = negate'; there's no general way for the compiler to do so, since it doesn't know the structure of your type.

Functions in Haskell, unlike, say, Prolog, only go from left of the = to the right of the =.  Thanks to referential transparency, you can go backwards from the point of view of proving properties about your code, but during evaluation term rewriting only happens from left to right.

  -- ryan