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
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@pobox.com
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
Greg Meredith wrote: 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
Is there documentation on the multi-parameter type classes?
Sections 7.4.2. Class declarations, 7.4.3 Functional dependencies and 7.4.4. Instance declarations of the GHC user guide give the short description of these features. These section refer to a couple of papers. The best explanation can be found in papers by Mark P. Jones: http://web.cecs.pdx.edu/~mpj/pubs.html (see especially `qualified types').
i think i see what you've done, but i'd like to read up on it to make sure that i understand.
The approach in the previous message was quite close to that used for representing collections. The type of a particular collection implies the type of collection's elements. In your case, the type of the agent implies the type of the processor for that particular agent (and vice versa). Incidentally, instance declarations can be recursive and mutually recursive.
Oleg,
Many thanks. i also found some course notes from Advance Functional
Programming at Utrecht very useful. i have to wait until i have quality time
to go over this because the next step is to close the final loop to find the
fix point of
- Process = Process(Nominate(Process))
i haven't worked out the correct instance syntax to express this idea. But,
i think the direction you pointed me in is the right one.
Best wishes,
--greg
On 4/22/07, oleg@pobox.com
Is there documentation on the multi-parameter type classes?
Sections 7.4.2. Class declarations, 7.4.3 Functional dependencies and 7.4.4. Instance declarations of the GHC user guide give the short description of these features. These section refer to a couple of papers. The best explanation can be found in papers by Mark P. Jones: http://web.cecs.pdx.edu/~mpj/pubs.html (see especially `qualified types').
i think i see what you've done, but i'd like to read up on it to make sure that i understand.
The approach in the previous message was quite close to that used for representing collections. The type of a particular collection implies the type of collection's elements. In your case, the type of the agent implies the type of the processor for that particular agent (and vice versa). Incidentally, instance declarations can be recursive and mutually recursive.
-- L.G. Meredith Managing Partner Biosimilarity LLC 505 N 72nd St Seattle, WA 98103 +1 206.650.3740 http://biosimilarity.blogspot.com
participants (2)
-
Greg Meredith -
oleg＠pobox.com