[Haskell-cafe] Re: haskell question

[oleg at pobox.com]

Greg Meredith wrote:
> The file compiles with ghc as is. If you uncomment the last
> section, however, you see that to close the loop on the constraints for the
> agent syntax we hit a typing error. i <b><i>think</i></b> this is a hard
> constraint in Haskell that prevents this level of generality in the
> specification, but maybe you can see a way around it.

I believe the Haskell typechecker is right

> instance (Eq n, Eq p) =>
>      CoreAgentSyntax (MinimalAgentSyntax n p) where
>       bind [] proc = Thunk (\() -> proc)
>
> data MinimalAgentSyntax n p =
>      Thunk (() -> p)
>      | Abstraction ([n] -> p)
>      | Concretion [n] p

The bind method has the signature

    bind :: (CoreProcessSyntax p, CoreAgentSyntax x) => [n] -> (p a x) -> x

That is: for any agent x and for _any_ process p (regardless of x), we
should be able to perform the bind operation. The signature for bind
proclaims total independence between 'p' and 'x'. However, when we
define the instance

>      CoreAgentSyntax (MinimalAgentSyntax n p) where
>       bind [] proc = Thunk (\() -> proc)

we see that process proc and the agent aren't totally independent: the
result of bind has the type 'MinimalAgentSyntax n process' and thus is
dependent on the 'process == p a x'. We have broken our previously
made independence proclamation, and so the typechecker rightfully
complaints. 

The following is one solution. It works sans the line marked TODO. I'm
not sure that line is correct:

--      -- TODO : lgm : need to substitute m for n in proc 
--      bind (name:names) proc = Abstraction (\m -> bind names proc) 

According to the type of Abstraction, 'bind names proc' should have
the type 'p', that is, the same type as proc. It should be a
process. OTH, bind returns an agent. Something is amiss here.


{-# OPTIONS -fglasgow-exts #-}

module Core where

-- What's in a name?

class Nominal n where
    nominate :: i -> n i

newtype Name i = Nominate i deriving Eq

instance Nominal Name where nominate i = Nominate i

-- Where are we?

class Locality a where
    locate :: (Eq s, Nominal n) => s -> (n i) -> a s (n i)
    name :: (Eq s, Nominal n) => a s (n i) -> (n i)

data Location s n = Locate s n deriving Eq

instance Locality Location where
   locate s n = Locate s n
   name (Locate s n) = n


-- Constraints

class CoreProcessSyntax p a x | p -> a x where
    zero :: p
    sequence :: a -> x -> p
    compose :: [p] -> p

class CoreAgentSyntax x p n | x -> p n where
    bind  :: [n] -> p -> x
    offer :: [n] -> p -> x 

-- Freedom (as in freely generated)

data MinimalProcessSyntax l x =
     Null
     | Sequence l x
     | Composition [MinimalProcessSyntax l x]

data MinimalAgentSyntax n p =
     Thunk (() -> p)
     | Abstraction ([n] -> p)
     | Concretion [n] p

-- Constraining freedom

instance CoreProcessSyntax (MinimalProcessSyntax l x) l x where
     zero = Null
     sequence l a = Sequence l a
     compose [] = zero
     compose ps = Composition ps

instance CoreAgentSyntax (MinimalAgentSyntax n p) p n where
      bind [] proc = Thunk (\() -> proc)

--      -- TODO : lgm : need to substitute m for n in proc 
--      bind (name:names) proc = Abstraction (\m -> bind names proc) 
      -- here's the possible implementation. I don't know if it's right.
      -- But at least it types
      bind (name:names) proc = Abstraction (\m -> comp $ bind names proc) 
          where comp (Thunk f) = f ()
                -- comp (Concretion n p) = ...
      offer names proc = Concretion names proc