On Wed, Dec 21, 2011 at 10:12 AM, Patrick Browne wrote:

On 21/12/11, *Richard O'Keefe * wrote:

So what exactly is the program supposed to do?

I am trying to see whether Haskell modules can be used for blending[1]. The original MAUDE [2,3] program just sets up an arbitrary meeting point, which is assumed to be time-2 and location-2. Then in MONK_MEETS_HIMSELF the up and down versions of these are made match. To do this I wish to declare the function location in MONK_ON_MOVE. Then I require different equations for that same location function in MONK_ON_MOVE_DOWN and MONK_ON_MOVE_UP both of which import MONK_ON_MOVE. Finally, I wish to import MONK_ON_MOVE_DOWN and MONK_ON_MOVE_UP into MONK_MEETS_HIMSELF and use the combined set of equations to check locations.

You can't do that in Haskell. All equations defining a function must occur contiguously in the same Haskell module. You've actually defined two separate functions, MONK_ON_MOVE_DOWN.location and MONK_ON_MOVE_UP.location. If you want to define a single function that blends their behaviors, you need to do that explicitly. For example, you might define these as partial functions, returning type "Maybe LocationOnPath", and then try each implementation (in your case, 2 tries), until one of them returns a non-Nothing result. You could use type classes with overlapping instances to try to merge two different definitions of location, but it wouldn't work the way you want. The compiler would statically choose one implementation of location that would be used for a given type, rather than trying equations from both (as you desire, and as would happen in Maude). So far I cannot figure out how the location function and the constructors

can be shared in this way using Haskell modules.

I have tried various combination import/export options, type classes, and newtype. I have also tried to use Strings instead of constructors.

I had trouble using Haskell equations with pure constructors. Due to my ignorance of Haskell semantics I am not sure what Constructor1 = Constructor2 means. But in the original Maude there are constructor only equations such as Timed2 = Timeu2 which in Maude means that the constructor Timed2 could be replaced with Timeu2. I wrote Haskell functions to try to achieve a similar effect e.g.

timed2 :: TimeOfDay -> TimeOfDay

timed2 Timed2 = Timeu2

I'm not sure why top-level equations like "Timed2 = Timeu2" (or even "Just () = Nothing") aren't an error in GHC (or even a -Wall warning), but, as you've observed, this won't cause Timed2 to rewrite to Timeu2. Constructors in Haskell truly are constructors, they don't rewrite to something else (similar to the intention of the [ctor] annotation in Maude). To make it work, you'd have to manually separate out which of your terms are truly constructors and which ones are functions. Then write equations defining the functions. Be sure that all equations for a given function are in a given place. You could of course implement a rewrite system on top of Haskell, and the syntax probably wouldn't be that bad (someone's probably already done it). But you can't directly write Maude-style rewrite systems in Haskell; the two languages just work differently. [1] http://cseweb.ucsd.edu/~goguen/pps/taspm.pdf

[2] http://lists.cs.uiuc.edu/pipermail/maude-help/2010-December/000456.html [3] http://lists.cs.uiuc.edu/pipermail/maude-help/2010-December/000462.html