[Haskell-cafe] Re: haskell question
oleg at pobox.com
oleg at pobox.com
Fri Apr 20 04:09:15 EDT 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
More information about the Haskell-Cafe
mailing list