Maude-help mailing list

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

Michael,
Thanks for informative feedback,
I agree that these are very different mechanisms. In this particular
case the relation between Haskell classes and Maude modules is that they
can both be used to enforce pairs of legal types (or sorts) before the
functions are actually written.  In the Maude example the sorts are left
open and the views express some legal pairings, which represent the
designer’s intention. Similarly for Haskell, the type variables in the
type class means that the types are left open until we make design
decisions at instance creation time. In short I am trying to enforce a
set of legal pairings at design time using Haskell instance or using
Maude views. The fundep (| a -> b) in Haskell prevents b from being a
free type variable. When we know the type of a then the result type
should be determined from that information alone. We do not want to fix
the type of a or b, but when we decided on some a then we want to fix an
appropriate b. I think that the views (V1, V2) help to do this. But it
is the user’s responsibility to construct the correct or appropriate
views in Maude or instances in Haskell.


Thanks again,
Pat



Michael Katelman wrote:
> 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
>>
>>


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