Maude-help mailing list

[Michael Katelman <katelman AT uiuc.edu>]

Patrick,

Sorry for such a belated reply.

Obviously, the details of the two systems are quite different, but at
a high-level I would say that maude's ad-hoc overloading mechanism
gets you the result you want, at least in this particular instance.
That is, I suppose I don't see why your above code is substantively
different from:

mod TEST is
including INT .
including STRING .

op spatialLocation : Int -> String .
op spatialLocation : String -> Int .
op spatialLocation : String -> String . --- optional, like your V3,
and when enabled results in a warning.
eq spatialLocation(1) = "one" .
eq spatialLocation("one") = 1 .
endm

To be honest, I don't really see what in maude is analogous to plain
type classes, let alone fundeps. maude does allow ad-hoc overloading,
of course, but the other use of type classes is to qualify polymorphic
functions, which maude doesn't really have. There is this "poly"
thing, but rewriting logic's type system is not polymorphic. To me,
the two are quite different, each with some aspects that the other
doesn't not support in a direct way.

-Mike
p.s. If you haven't already, you maybe interested to read how type
classes get compiled away into plain system F. That is, type classes
are just syntactic sugar, not particularly special. I am not sure of
the exact reference, but maybe it's this one:

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.5615

My understanding is that they become compiled into record types, with
fields holding the functions that comprise that instance of the class.



On Thu, Jul 1, 2010 at 8:23 AM, Patrick Browne 
<patrick.browne AT dit.ie>
 wrote:
> 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") .
>
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/maude-help
>
>