Maude-help mailing list

[Patrick Browne <patrick.browne AT dit.ie>]

Hi,
I am doing a practical comparison between Maude and Haskell.
I have attempted to implement the Haskell functional dependency feature
in Maude.
Any comments or assistance would be appreciated.

Regards,
Pat

This message has been scanned for content and viruses by the DIT Information 
Services E-Mail Scanning Service, and is believed to be clean. 
http://www.dit.ie
{- C:\GHC\ghc-6.8.3\bin\ghci.exe  -XMultiParamTypeClasses 
-XFunctionalDependencies -fglasgow-exts -fallow-undecidable-instances



My understanding of functional dependencies is that they can be used to 
ensure that one type depends on another type.
For example, the type of location depends could on the type of the object at 
that location. 
Consider two models 
1) The location of an aircraft landing should have location of the type 
AirportCode, 
2) The location of a car's destination should have a type 
CartesianCoordinate. 

AirportCodes should not be used as locations in 2) and CartesianCoordinates 
should not be used as locations in 1).
Haskell class, instances, and fundeps were used to represent the above 
requirements. 
I generalized the requirement a bit, testing on a varietyof types (below). 
Obviously, some cases are ambigious and/or conflicting and the Haskell 
compiler correctly flags this.

I am trying to replicate this functionality in the Maude file 
FundepMaude.maude

-}

class LocatedAt object location | object -> location where
 spatialLocation :: object -> location


-- 1) Haskell does not know exact type for the literal 1, hence a cast. 
instance LocatedAt  Int  String  where
 spatialLocation(1::Int)="home"

-- 2) 
instance LocatedAt String Int where
 spatialLocation("home")=1

-- 3) Compiles and runs  OK, but obviously not in conjunction with 2
-- instance LocatedAt  String  String  where
--  spatialLocation("home")="home"
  
-- 4) Compiles and runs OK
instance LocatedAt  Bool  String  where
  spatialLocation(True)="home"





*** Below is my attempt at functional dependencies in Maude
*** I am trying to capture the same semantics as in the file FundepHaskell.hs

*** A generic theory, containing abstract sorts
fth FD is
sorts Object Location .
endfth

*** concrete sorts
mod FDC  is
protecting INT .
protecting STRING .
endm


*** We can constrain the sort pairs using views, which I think are analogous 
to Haskell's functional dependency
view V1 from FD to FDC is
sort Object to String  .
sort Location to  Int .
endv

view V2 from FD to FDC is
sort Location to  String .
sort Object to Int .
endv

*** V3 will cause problems, which, in relation trying to implement Haskell 
fundeps, is desirable
*** If included in TEST then Maude will issue warning: unusable view V3 while 
evaluating module instantiation LOCATEDAT{V3}
*** But Maude permits the running of the function: red spatialLocation("one") 
even with the V3 loaded
*** In contrast CafeOBJ (with V3 loaded) gives no warning, but will give an 
ambigious parse to red spatialLocation("one")  .
view V3 from FD to FDC is
sort Location to  String .
sort Object to String .
endv


*** This parameterized module is analogous to the Haskell LocatedAt class
mod LOCATEDAT{P :: FD} is
op  spatialLocation : P$Object -> P$Location  .
endm


mod TEST is
protecting LOCATEDAT{V1} .
protecting LOCATEDAT{V2} .
protecting LOCATEDAT{V3} .
eq spatialLocation(1) = "one" .
eq spatialLocation("one") = 1 .
endm
eof

*** The following execute as expected
red spatialLocation(1)  .
red spatialLocation("one") .