[Haskell-cafe] Re: haskell question

[Greg Meredith]

Oleg,

Many thanks for your help! i notice that the code you sent requires
-fglasgow-exts to be syntactically correct. Is there documentation on the
multi-parameter type classes? i think i see what you've done, but i'd like
to read up on it to make sure that i understand.

Best wishes,

--greg

On 4/20/07, oleg at pobox.com <oleg at pobox.com> wrote:
>
>
> 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
>
>


-- 
L.G. Meredith
Managing Partner
Biosimilarity LLC
505 N 72nd St
Seattle, WA 98103

+1 206.650.3740

http://biosimilarity.blogspot.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20070420/8e2f41e1/attachment.htm