[Haskell-cafe] Re: haskell question

20 Apr 2007

      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

[Haskell-cafe] Re: haskell question

oleg＠pobox.com