[Haskell-cafe] second order types
Is a second order type one whose instances (values?) are ordinary types?Are kinds *-* second order types?Is Species without the argument a second order type?But with the argument Species is a first order type?Thanks,Pat-- Elephant and Dog typesdata Elephant = Elephant deriving Showdata Dog = Dog deriving Show-- The LHS Species a is a type constructor?data Species a = Species a deriving Show-- is-a means “Dog is a species” rather than “Fido is a dog” class Taxonomy f where isA::f a - a instance Taxonomy Species where isA (Species x) = x{-isA (Species Elephant) isA (Species Dog):t Species Dog === Species Dog :: Species Dog:k Species Dog === Species Dog :: *:k Species === Species :: * - *((isA (Species Elephant))::Species) === Expecting an ordinary type, but found a type of kind * - *-}
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Is there a Galois correspondence between a Haskell class hierarchy and a given instance hierarchy?
HiIs it reasonable to consider a Haskell class as a loose signature-only-specification (denoting a theory) and an instance as an implementation (denoting a model)?In the example below the specification of the class BUILDING is textually smaller than the specification of the class HOUSE,provided we consider the operation inherited by HOUSE from BUILDING to be part of the signature of HOUSE (this may not be a valid assumption). Is there a Galois correspondence between a Haskell class hierarchy and a given instance hierarchy for a particular type?So more details are explained as [1 ,2 ].Pat--General Idea-- Theory subTheory Theory' = Model' subModel Model--A specific example with Haskell class-to-instance relation --class(BUILDING) subTheory class(HOUSE) = instance(HOUSE)} subModel instance(BUILDING) data House = House deriving Show data Building = Building deriving Show class BUILDING building where -- specify the behavior of buildings here, if any supportRoof :: building - String class BUILDING house = HOUSE house where -- specify additional behavior of houses here, if any live::house - Bool instance BUILDING Building where -- specify how the type Building implements the behavior of type class BUILDING supportRoof b = BUILDING.Building -- A particular b which is a BUILDING.Building.particular can support a roof instance BUILDING House where supportRoof h = BUILDING.House -- A particular h which is a BUILDING.House.particular can support a roof instance HOUSE House where -- specify how the type House implements the behaviour of type class HOUSE live h = if ((supportRoof h) == BUILDING.House) then True else False -- An particular h HOUSE.House.particular can support a roof in exactly the same way as BUILDING.House.particular can. instance HOUSE Building where -- specify how the type Building implements the behaviour of type class HOUSE live b = if ((supportRoof b) == BUILDING.Building) then True else False -- An particular b HOUSE.Building.particular can support a roof in exactly the same way as BUILDING.Building.particular can. Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Understanding version differences
Hi,The code [1] below compiles and runs with GHCi version 7.0.4.I get one warning and an error message with GHCi version 7.6.1.1) Warning -XDatatypeContexts is deprecated. Unless there are propagation effects, this is well explained.2) foom-1.hs:65:15: `quality' is applied to too many type arguments In the type `quality entity - agent - IO Observation' In the class declaration for `OBSERVERS'Failed, modules loaded: none.I do not understand the error message from 7.6.1. I am not too interested actually fixing it, I just want to understand it.Thanks,Pat[1]The code is from: A Functional Ontology of Observation and Measurement Werner Kuhn{-# LANGUAGE DatatypeContexts,MultiParamTypeClasses #-}module ENDURANTS whereimport System.Timetype Id = Stringtype Position = Integertype Moisture = Floattype Celsius = Stringtype Heat = Float data WeatherStation = WeatherStation Id Position deriving Showdata Value = Boolean Bool | Count Int | Measure Float | Category String deriving Showdata Observation = Observation Value Position ClockTime deriving Showdata AmountOfAir = AmountOfAir Heat Moisture deriving ShowmuensterAir = AmountOfAir 10.0 70.0class ENDURANTS endurant where -- must add instances all down the hierarchy for each instanceinstance ENDURANTS WeatherStation whereinstance ENDURANTS AmountOfAir whereclass ENDURANTS physicalEndurant = PHYSICAL_ENDURANTS physicalEndurant whereinstance PHYSICAL_ENDURANTS WeatherStation whereinstance PHYSICAL_ENDURANTS AmountOfAir whereclass PHYSICAL_ENDURANTS amountOfMatter = AMOUNTS_OF_MATTER amountOfMatter whereinstance AMOUNTS_OF_MATTER WeatherStation whereclass PHYSICAL_ENDURANTS physicalObject = PHYSICAL_OBJECTS physicalObject whereinstance PHYSICAL_OBJECTS WeatherStation whereclass PHYSICAL_OBJECTS apo = APOS apo where getPosition :: apo - Positioninstance APOS WeatherStation where getPosition (WeatherStation iD pos) = pos + 10 -- a data type declaration and data type constructor.data PHYSICAL_ENDURANTS physicalEndurant = Temperature physicalEndurant = Temperature physicalEndurant deriving Show-- Qualities the class of all quality types (= properties) is a constructor class-- its constructors can be applied to endurants, perdurants, qualities or abstractsclass QUALITIES quality entity instance QUALITIES Temperature AmountOfAirclass (APOS agent, QUALITIES quality entity) = OBSERVERS agent quality entity where observe :: quality entity - agent - IO Observation express :: quality entity - agent - Value observe quale agent = do clockTime - getClockTime return (Observation (express quale agent) (getPosition agent) clockTime)instance OBSERVERS WeatherStation Temperature AmountOfAir where express (Temperature (AmountOfAir heat moisture)) weatherStation = Measure heat {--- running the followingexpress (Temperature (AmountOfAir 40 20)) (WeatherStation rr 6)-- GivesMeasure 40.0 Measure 40.0-- We can get the type: Value :t express (Temperature (AmountOfAir 40 20)) (WeatherStation rr 6)-}
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Understanding version differences
Thanks to Roman and Eric for for their clear explanations.PatOn 09/07/13, Roman Cheplyaka r...@ro-che.info wrote:The compiler defaults the kind of 'quality' (i.e. the first argument ofQUALITIES) to *, not being able to infer it from the class definitionitself (and other definitions that it references).Since you want it to have kind * - *, you should enable KindSignaturesand add an annotation, or otherwise disambiguate the kind.This behaviour follows the Haskell Report. The change from previousversions of GHC is documented here:http://www.haskell.org/ghc/docs/7.4.1/html/users_guide/release-7-4-1.html#id3015054Roman* Patrick Browne patrick.bro...@dit.ie [2013-07-09 12:45:19+0100] Hi, The code [1] below compiles and runs with GHCi version 7.0.4. I get one warning and an error message with GHCi version 7.6.1. 1) Warning -XDatatypeContexts is deprecated. Unless there are propagation effects, this is well explained. 2) foom-1.hs:65:15: `quality' is applied to too many type arguments In the type `quality entity - agent - IO Observation' In the class declaration for `OBSERVERS' Failed, modules loaded: none. I do not understand the error message from 7.6.1. I am not too interested actually fixing it, I just want to understand it. Thanks, Pat [1]The code is from: A Functional Ontology of Observation and Measurement Werner Kuhn {-# LANGUAGE DatatypeContexts,MultiParamTypeClasses #-} module ENDURANTS where import System.Time type Id = String type Position = Integer type Moisture = Float type Celsius = String type Heat = Float data WeatherStation = WeatherStation Id Position deriving Show data Value = Boolean Bool | Count Int | Measure Float | Category String deriving Show data Observation = Observation Value Position ClockTime deriving Show data AmountOfAir = AmountOfAir Heat Moisture deriving Show muensterAir = AmountOfAir 10.0 70.0 class ENDURANTS endurant where -- must add instances all down the hierarchy for each instance instance ENDURANTS WeatherStation where instance ENDURANTS AmountOfAir where class ENDURANTS physicalEndurant = PHYSICAL_ENDURANTS physicalEndurant where instance PHYSICAL_ENDURANTS WeatherStation where instance PHYSICAL_ENDURANTS AmountOfAir where class PHYSICAL_ENDURANTS amountOfMatter = AMOUNTS_OF_MATTER amountOfMatter where instance AMOUNTS_OF_MATTER WeatherStation where class PHYSICAL_ENDURANTS physicalObject = PHYSICAL_OBJECTS physicalObject where instance PHYSICAL_OBJECTS WeatherStation where class PHYSICAL_OBJECTS apo = APOS apo where getPosition :: apo - Position instance APOS WeatherStation where getPosition (WeatherStation iD pos) = pos + 10 -- a data type declaration and data type constructor. data PHYSICAL_ENDURANTS physicalEndurant = Temperature physicalEndurant = Temperature physicalEndurant deriving Show -- Qualities the class of all quality types (= properties) is a constructor class -- its constructors can be applied to endurants, perdurants, qualities or abstracts class QUALITIES quality entity instance QUALITIES Temperature AmountOfAir class (APOS agent, QUALITIES quality entity) = OBSERVERS agent quality entity where observe :: quality entity - agent - IO Observation express :: quality entity - agent - Value observe quale agent = do clockTime - getClockTime return (Observation (express quale agent) (getPosition agent) clockTime) instance OBSERVERS WeatherStation Temperature AmountOfAir where express (Temperature (AmountOfAir heat moisture)) weatherStation = Measure heat {- -- running the following express (Temperature (AmountOfAir 40 20)) (WeatherStation rr 6) -- Gives Measure 40.0 Measure 40.0 -- We can get the type: Value :t express (Temperature (AmountOfAir 40 20)) (WeatherStation rr 6) -} Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. [1]http://www.dit.ie This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. [2]http://www.dit.ie References 1. http://www.dit.ie/ 2. http://www.dit.ie/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
Re: [Haskell-cafe] Subclass or no subclass?
On 30/06/13, Dan Burton danburton.em...@gmail.com wrote:I am not trying to say every building is a shelter, rather anything that is a building must provide sheltering services. Well if it walks like a shelter and quacks like a shelter... /shrugOne of the nice things about OO is the intuitive nature of the is-a relation between class and instance (forgetting hierarchies for the moment). I suggest that an intuitive interpretation of the Haskell class–instance relation might be *acts-as*. For example, a car or a bus could afford transport once they have a move operation. This is an intuitive view for design; it does not reflect the language level function of handling ad-hoc polymorphism. Also it reifies the type class, which AFAIK does not exist at run time. Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Subclass or no subclass?
As you say if I omit references to superclass methods in the subclasses then I get different compile time behaviour.But then the question is that if a putative subclass has no reference to superclass methods should it be a subclass at all?I deliberately want to model the case where each subclass depends on the superclass.Hence, I have arranged that each subclass method calls a superclass method. If I remove the references to the superclass methods would that indicate that I do not need the superclass?It seems that if a method is invoked in a class instance then there must exist a definition of that method somewhere (not necessarily in the class/instance hierarchy). Where there exists a genuine sub/super relation, is there a case where the compiler will not catch the implicit superclass (WithoutSubclass) and *must* have the explicit class hierarchy (WithoutSubclass).The above represents my attempts to understand the semantics of Haskell sub/super-classes. I may have missed something obvious.Thanks,PatOn 29/06/13, Richard Eisenberg e...@cis.upenn.edu wrote:Yes, the runtime behavior should be the same between those modules. But, the compile-time behavior is not. The superclass constraints in your first version mean that every instance of, say, Building *must* be accompanied by an instance of Shelter, regardless of the implementation of that instance. This would be easiest to see if your implementations did not call any functions, but just returned strings. With that change, in your second version, you could remove the instance for Shelter and everything would still compile. However, in the first, removing that instance would cause compile-time failures for the others, as the superclass constraint would not be satisfied.I hope this helps!RichardOn Jun 29, 2013, at 12:46 PM, Patrick Browne wrote:Hi,The runtime behaviour of the two modules below *seems* to be the same.Is this correct? I am not trying to say every building is a shelter, rather anything that is a building must provide sheltering services.I think that the use of sub-classes makes this explicit, but it *seems* that one gets the same results without the subclass.Any clarification welcome.Regards,Pat-- module WithSubclass wheredata SomeWhereToShelter = SomeWhereToShelter class Shelter shelter where s :: shelter - Stringclass Shelter building = Building building where b :: building - Stringclass Shelter house = House house where h :: house - Stringinstance Shelter SomeWhereToShelter where s x = Shelters afford basic sheltering instance Building SomeWhereToShelter where b x = (s x) ++ , Buildings afford better shelteringinstance House SomeWhereToShelter where h x = (s x) ++ (b x) ++ , Houses afford even better sheltering-- ===module WithoutSubclass wheredata SomeWhereToShelter = SomeWhereToShelter class Shelter shelter where s :: shelter - Stringclass Building building where b :: building - Stringclass House house where h :: house - Stringinstance Shelter SomeWhereToShelter where s x = Shelters afford basic sheltering instance Building SomeWhereToShelter where b x = (s x) ++ , Buildings afford better shelteringinstance House SomeWhereToShelter where h x = (s x) ++ (b x) ++ , Houses afford even better sheltering Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___Haskell-Cafe mailing listHaskell-Cafe@haskell.org Haskell-Cafe@haskell.orghttp://www.haskell.org/mailman/listinfo/haskell-cafe Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Subclass or no subclass?
Richard,Yes, that example makes things clear.Thanks,PatOn 30/06/13, Richard Eisenberg e...@cis.upenn.edu wrote:It sounds like the following example may help: class A alpha where a :: alpha - Int class A beta = B beta where b :: beta - Int class C gamma where c :: gamma - Int foo :: B beta = beta - Int foo x = a x + b x -- the (A beta) is implied by the superclass constraint) bar :: C gamma = gamma - Int bar x = a x + c x -- ERROR: no instance of A gammaThe superclass constraint A beta = B beta means that anywhere a B beta constraint is written, the constraint A beta is inferred. For this all to work out, it also means that any instance of B must be coupled with an instance for A.Does this help clarify?RichardOn Jun 30, 2013, at 1:46 PM, Patrick Browne wrote:As you say if I omit references to superclass methods in the subclasses then I get different compile time behaviour.But then the question is that if a putative subclass has no reference to superclass methods should it be a subclass at all?I deliberately want to model the case where each subclass depends on the superclass.Hence, I have arranged that each subclass method calls a superclass method. If I remove the references to the superclass methods would that indicate that I do not need the superclass?It seems that if a method is invoked in a class instance then there must exist a definition of that method somewhere (not necessarily in the class/instance hierarchy). Where there exists a genuine sub/super relation, is there a case where the compiler will not catch the implicit superclass (WithoutSubclass) and *must* have the explicit class hierarchy (WithoutSubclass).The above represents my attempts to understand the semantics of Haskell sub/super-classes. I may have missed something obvious.Thanks,PatOn 29/06/13, Richard Eisenberg e...@cis.upenn.edu e...@cis.upenn.edu wrote:Yes, the runtime behavior should be the same between those modules. But, the compile-time behavior is not. The superclass constraints in your first version mean that every instance of, say, Building *must* be accompanied by an instance of Shelter, regardless of the implementation of that instance. This would be easiest to see if your implementations did not call any functions, but just returned strings. With that change, in your second version, you could remove the instance for Shelter and everything would still compile. However, in the first, removing that instance would cause compile-time failures for the others, as the superclass constraint would not be satisfied.I hope this helps!RichardOn Jun 29, 2013, at 12:46 PM, Patrick Browne wrote:Hi,The runtime behaviour of the two modules below *seems* to be the same.Is this correct? I am not trying to say every building is a shelter, rather anything that is a building must provide sheltering services.I think that the use of sub-classes makes this explicit, but it *seems* that one gets the same results without the subclass.Any clarification welcome.Regards,Pat-- module WithSubclass wheredata SomeWhereToShelter = SomeWhereToShelter class Shelter shelter where s :: shelter - Stringclass Shelter building = Building building where b :: building - Stringclass Shelter house = House house where h :: house - Stringinstance Shelter SomeWhereToShelter where s x = Shelters afford basic sheltering instance Building SomeWhereToShelter where b x = (s x) ++ , Buildings afford better shelteringinstance House SomeWhereToShelter where h x = (s x) ++ (b x) ++ , Houses afford even better sheltering-- ===module WithoutSubclass wheredata SomeWhereToShelter = SomeWhereToShelter class Shelter shelter where s :: shelter - Stringclass Building building where b :: building - Stringclass House house where h :: house - Stringinstance Shelter SomeWhereToShelter where s x = Shelters afford basic sheltering instance Building SomeWhereToShelter where b x = (s x) ++ , Buildings afford better shelteringinstance House SomeWhereToShelter where h x = (s x) ++ (b x) ++ , Houses afford even better sheltering Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___Haskell-Cafe mailing listHaskell-Cafe@haskell.org Haskell-Cafe@haskell.org Haskell-Cafe@haskell.org Haskell-Cafe@haskell.orghttp://www.haskell.org/mailman/listinfo/haskell-cafe Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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
[Haskell-cafe] Subclass or no subclass?
Hi,The runtime behaviour of the two modules below *seems* to be the same.Is this correct? I am not trying to say every building is a shelter, rather anything that is a building must provide sheltering services.I think that the use of sub-classes makes this explicit, but it *seems* that one gets the same results without the subclass.Any clarification welcome.Regards,Pat-- module WithSubclass wheredata SomeWhereToShelter = SomeWhereToShelter class Shelter shelter where s :: shelter - Stringclass Shelter building = Building building where b :: building - Stringclass Shelter house = House house where h :: house - Stringinstance Shelter SomeWhereToShelter where s x = Shelters afford basic sheltering instance Building SomeWhereToShelter where b x = (s x) ++ , Buildings afford better shelteringinstance House SomeWhereToShelter where h x = (s x) ++ (b x) ++ , Houses afford even better sheltering-- ===module WithoutSubclass wheredata SomeWhereToShelter = SomeWhereToShelter class Shelter shelter where s :: shelter - Stringclass Building building where b :: building - Stringclass House house where h :: house - Stringinstance Shelter SomeWhereToShelter where s x = Shelters afford basic sheltering instance Building SomeWhereToShelter where b x = (s x) ++ , Buildings afford better shelteringinstance House SomeWhereToShelter where h x = (s x) ++ (b x) ++ , Houses afford even better sheltering Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Propositions in Haskell
I do understand the difference between theorem provers and Haskell programs.Logic can be used to reason 'about' Haskell programs and logic can be used 'within' Haskell programs.I am trying to clarify the difference between 'about' and 'within'Is approach 1 concerned with |= (model based 'within'), whereas approach 2 is concerned with |- (proof based 'about')?Thanks,PatOn 15/05/13, Alberto G. Corona agocor...@gmail.com wrote:Not exactly what you ask, but it is noteworthy that the mind has different logic processors. The fastest one work with IF THEN ELSE rules applied specifically to deals. This is why your example (and most examples of logic) involves a kind of deal expressed in the first person. This trigger a fast mental evaluation, while an equivalent but more general case is harder to process and need some paper work. (That special treatment of first person deals logic respond to the need to detect breaks of deals as fast as possible) http://en.wikipedia.org/wiki/Wason_selection_taskThat's why higher level languages have redundant logical structures and do not follow a general abstract and short mathematical notation. Therefore higher level, in programming languages, does not mean higher mathematical abstraction, but to be closer to the way the mind works. 2013/5/15 Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie -- Hi-- I am trying to show that a set of propositions and a conclusion the form a valid argument.-- I used two approaches; 1) using if-then-else, 2) using pattern matching. -- The version using if-then-else seems to be consistent with my knowledge of Haskell and logic (either of which could be wrong).-- Can the second approach be improved to better reflect the propositions and conclusion? Maybe type level reasoning could be used? -- -- Valid argument?-- 1. I work hard or I play piano-- 2. If I work hard then I will get a bonus-- 3. But I did not get a bonus-- Therefore I played piano-- Variables: p = Piano, w = worked hard, b = got a bonus -- (w \/ p) /\ (w = b) /\ ¬(b)-- --- -- p -- First approach using language control structure if-then-elsew, p, b::Bool-- Two equivalences for (w \/ p) as an implication. -- 1. (w \/ p) =equivalent-to= (not p) = w-- 2. (w \/ p) =equivalent-to= (not w) = p-- Picked 2p = if (not w) then True else False -- Contrapositive: (w = b) =equivalent-to= ~b = ~w w = if (not b) then False else Trueb = False -- gives p is true and w is false-- Second approach using pattern matching -- I think the rewriting goes from left to right but the logical inference goes in the opposite direction. w1, p1, b1::Boolp1 = (not w1) w1 = b1 -- Not consistent with statements, but I do not know how to write ~b1 = ~w1 in Haskellb1 = False-- Again gives p1 is true and w1 is false Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe -- Alberto. Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Propositions in Haskell
-- Hi-- I am trying to show that a set of propositions and a conclusion the form a valid argument.-- I used two approaches; 1) using if-then-else, 2) using pattern matching.-- The version using if-then-else seems to be consistent with my knowledge of Haskell and logic (either of which could be wrong).-- Can the second approach be improved to better reflect the propositions and conclusion? Maybe type level reasoning could be used?-- -- Valid argument?-- 1. I work hard or I play piano-- 2. If I work hard then I will get a bonus-- 3. But I did not get a bonus-- Therefore I played piano-- Variables: p = Piano, w = worked hard, b = got a bonus-- (w \/ p) /\ (w = b) /\ ¬(b)-- --- -- p -- First approach using language control structure if-then-elsew, p, b::Bool-- Two equivalences for (w \/ p) as an implication.-- 1. (w \/ p) =equivalent-to= (not p) = w-- 2. (w \/ p) =equivalent-to= (not w) = p-- Picked 2p = if (not w) then True else False -- Contrapositive: (w = b) =equivalent-to= ~b = ~ww = if (not b) then False else Trueb = False -- gives p is true and w is false-- Second approach using pattern matching -- I think the rewriting goes from left to right but the logical inference goes in the opposite direction.w1, p1, b1::Boolp1 = (not w1) w1 = b1 -- Not consistent with statements, but I do not know how to write ~b1 = ~w1 in Haskellb1 = False-- Again gives p1 is true and w1 is false Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Propositions in Haskell
The relation to theorem proving is the main motivation for my question. In am trying to understand why some equations are ok and others not. I suspect that in Haskell equations are definitions rather than assertions. If approach 2 is a non-starter in Haskell, then can approach 1, using if-then-else, achieve the same results for propositions? ThanksPatOn 15/05/13, Dan Mead d.w.m...@gmail.com wrote:i don't understand what you're trying to do with that code, however you seem to be asking about theorem proving in generalcheck outhttp://www.haskell.org/haskellwiki/Libraries_and_tools/Theorem_provers and http://en.wikipedia.org/wiki/Automated_theorem_provinghope it helps On Wed, May 15, 2013 at 11:34 AM, Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie wrote: -- Hi-- I am trying to show that a set of propositions and a conclusion the form a valid argument.-- I used two approaches; 1) using if-then-else, 2) using pattern matching. -- The version using if-then-else seems to be consistent with my knowledge of Haskell and logic (either of which could be wrong).-- Can the second approach be improved to better reflect the propositions and conclusion? Maybe type level reasoning could be used? -- -- Valid argument?-- 1. I work hard or I play piano-- 2. If I work hard then I will get a bonus-- 3. But I did not get a bonus-- Therefore I played piano-- Variables: p = Piano, w = worked hard, b = got a bonus -- (w \/ p) /\ (w = b) /\ ¬(b)-- --- -- p -- First approach using language control structure if-then-elsew, p, b::Bool-- Two equivalences for (w \/ p) as an implication. -- 1. (w \/ p) =equivalent-to= (not p) = w-- 2. (w \/ p) =equivalent-to= (not w) = p-- Picked 2p = if (not w) then True else False -- Contrapositive: (w = b) =equivalent-to= ~b = ~w w = if (not b) then False else Trueb = False -- gives p is true and w is false-- Second approach using pattern matching -- I think the rewriting goes from left to right but the logical inference goes in the opposite direction. w1, p1, b1::Boolp1 = (not w1) w1 = b1 -- Not consistent with statements, but I do not know how to write ~b1 = ~w1 in Haskellb1 = False-- Again gives p1 is true and w1 is false Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] model theory for type classes
{-I am trying to apply model theoretic concepts to Haskell by considering type classes as theories and instances as models.Then the declaration of a sub-class specifies a signature morphism from the superclass to the subclass.In case below the theories (classes) are signature only (no default methods) so a signature morphisms can be considered as a theory morphisms.The only purpose of the code below is to explore the concepts of model expansion[1] and model reduct [2] in HaskellI am not trying to improve or rewrite the code itself for any particular application.Neither am I trying to find OO style inheritance semantics in Haskell type classes.Rather, I am wondering if the last instance of Worker (commented out) demonstrates that there is no model expansion in this case.That is, for theory morphism the theory(Person) = theory(Worker) we do not get (model(Person) sub-model model(Worker)).If there is no model expansion could it be because of the constructor discipline, which only allows variables, and constructors in the LHS argument patterns.[1] http://www.informatik.uni-bremen.de/~cxl/papers/wadt04b.pdf[2] http://en.wikipedia.org/wiki/Reduct-}constant::Intconstant = (1::Int)fun1::Int - Intfun1 (constant::Int) = 8class Person i n | i - n where pid :: i name :: i - n-- There is a signature/theory morphism from Person to Workerclass Person i n = Worker i n s | i - s where salary :: i - s -- model(Person)instance Person Int [Char] where pid = (1::Int) name (1::Int) = (john::[Char])-- We can say that a model(Worker) can use model(Person).instance Worker Int [Char] Int where-- Hypothesis: pid on the RHS shows that a model(Person) is *available* in model(Person) (reduct)? salary i = if i == pid then 100 else 0 -- instance Worker Int [Char] Int where-- Hypothesis: The model of Person cannot be expanded to a model of Worker(no model expansion)-- pid below is not inherited from Person, it is just a local variable-- salary pid = 100
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] model theory for type classes
On 23/08/12, Brent Yorgey byor...@seas.upenn.edu wrote:fun1 returns 8 for all inputs. The fact that fun1's definition usesthe name 'constant' which happens to have the same name as somethingin scope is irrelevant. For example, this is precisely the same as the above:constant :: Intconstant = 1fun1 :: Int - Intfun1 foo = 8-BrentYes, I am aware the semantics of Haskell is this situation. I also know for every model of a subclass there must exist a model of the super-class. I am just not sure whether there is a model expansion from the super-class model to the subclass model.I am also unsure of the morphism from type variables in the class definition to actual types in instances and to the operations in the instance.In a intuitive way I think that I understand these things, but not in a model theoretic way. Thanks, Pat Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 3 level hierarchy of Haskell objects
On 09/08/12, Jay Sulzberger j...@panix.com wrote:Here we are close to the distinction between a class of objectswhich satisfy a condition vs objects with added structure, forwhich see: http://math.ucr.edu/home/baez/qg-spring2004/discussion.html http://ncatlab.org/nlab/show/stuff,+structure,+propertyoo--JS.This seems to be addressing my my question, but I am not sure that I can relate the above ideas to Haskell.Below is my current (naive) understanding and some further question:objects which satisfy a condition Could these objects be models that have the same signature (instances in Haskell). Haskell type classes seem to be signature only (no equations, ignoring default methods) so in general they provide an empty theory with no logical consequences.objects with added structureI am struggling with this concept both in general and in relation to the hierarchy from my earlier posting.Could this be model expansion where a theory describing an existing model is enriched with additional axioms.The enriched theory is then satisfied by models with more structure (operations).I am unsure about the size of this expanded model and the number of potential expanded models. Would a expanded model have less elements?Would there be fewer models for the enriched theory?In relation to Haskell data types also have structure (constructors). The data types can be used to build other data types (is this model expansion?)I am not sure if the model (instance) of a sub-class could be considered as expanded model of its super-class.Your reply was very helpfulThanks,Pat Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] 3 level hierarchy of Haskell objects
Gast [1] describes a 3 level hierarchy of Haskell objects using elementOf from set theory:value *elementOf* type *elementOf* classQuestionIf we include super-classes would the following be an appropriate mathematical representation?value *elementOf* type *elementOf* class *subSet* super-classMaybe instantiated classes would make more sense in the hierarchy?My thinking is that values and types and instances are concrete whereas classes are not.Regards,Pat[1] bib.informatik.uni-tuebingen.de/files/wsi-berichte/wsi-99-5.ps.gz Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 3 level hierarchy of Haskell objects
On 08/08/12, Ertugrul Söylemez e...@ertes.de wrote: If we include super-classes would the following be an appropriate mathematical representation?What is a superclass? What are the semantics?I assume that like a normal class a super-class *defines* a set operations for types, but it is not *a set* of types.A sub-class can use the signature and default methods of its super-class.I have no particular super-class in mind.Rather I am trying to make sense of how these Haskell objects are mathematically related.Regards,Pat Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 3 level hierarchy of Haskell objects
On 08/08/12, Ertugrul Söylemez e...@ertes.de wrote:So you basically just mean class (Functor f) = Applicative fYes, but I want to know if there is a simple mathematical relation between the classes and/or their typesBut from your emails the original hierarchy seems to have been superseded, and my expectation of a simple set-theoretic relation is a bit naive.Thanks,Pat Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
Ertugrul,Thank you for your detailed and helpful reply.I was unaware of the distinction between data/value and type constructors.Regards,PatOn 31/07/12, Ertugrul Söylemez e...@ertes.de wrote:Patrick Browne patrick.bro...@dit.ie wrote: Thanks for all the very useful feed back on this thread. I would like to present my possibly incorrect summarized view: Class signatures can contain placeholders for constructors. These place-holder-constructors cannot be used in the class to define functions (I assume other in-scope constructors can be used). In the instance a real constructor can be substituted for the place-holder-constructor. Does this restrict the type of equation that can be used in a type class? It seems that some equations respecting the constructor discipline are not allowed.Your intuition seems to be near the truth, although your terminology iscurrently wrong. Let's look at an example: class Functor f where fmap :: (a - b) - (f a - f b)The 'f' in the class header is probably what you call a placeholder forconstructors. This is not a placeholder, but a type variable. Itrepresents a type. Incidentally in this case it indeed represents aconstructor, namely a /type/ constructor (like Maybe). This is animportant distinction, because generally when we talk aboutconstructors, we mean /value/ constructors (like Just or Nothing): data Maybe a = Just a | NothingHere Maybe is a type constructor. This is because it's not a type inits own right, but is applied to another type (like Int) to yield anactual type (Maybe Int). The type Maybe is applied to is representedby the type variable 'a' in the code above. To simplify communicationwe often call Maybe itself also a type, but it's really not.Let's write the Functor instance for Maybe. It is common to use ahelper function (a so-called fold function), which allows us to expressmany operations more easily. It's called 'maybe' for Maybe: maybe :: b - (a - b) - Maybe a - b maybe n j (Just x) = j x maybe n j Nothing = n instance Functor Maybe where fmap f = maybe Nothing (Just . f)This is the instance for Maybe. The type variable 'f' from the classnow becomes a concrete type constructor Maybe. In this instance youhave f = Maybe, so the type of 'fmap' for this particular instancebecomes: fmap :: (a - b) - (Maybe a - Maybe b)The notable thing here is that this is really not aplaceholder/replacement concept, but much more like a function andapplication concept. There is nothing that stops you from having typevariables in an instance: instance Functor (Reader e) whereAs you can see there is still what you called a placeholder in thisinstance, so the placeholder concept doesn't really make sense here.The declaration can be read as: For every type 'e' the type 'Reader e' is an instance of the Functor type class. I appreciate that in Haskell the most equations occur in the instances, [...]Not at all. When programming Haskell you write lots and lots ofequations outside of class instances. Whenever you write = youintroduce an equation, for example in top-level definitions and in 'let'and 'where' bindings. [...] but from my earlier post: I merely wish to identify the strengths and weakness of *current Haskell type classes* as a pure *unit of specification*I think you will be interested in this Stack Overflow answer: http://stackoverflow.com/a/8123973Even though the actual question answered is different, it does give anice overview of the strengths and weaknesses of type classes.Greets,Ertugrul-- Not to be or to be and (not to be or to be and (not to be or to be and(not to be or to be and ... that is the list monad. Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
Hi,Thanks for all the very useful feed back on this thread.I would like to present my possibly incorrect summarized view:Class signatures can contain placeholders for constructors.These place-holder-constructors cannot be used in the class to define functions (I assume other in-scope constructors can be used). In the instance a real constructor can be substituted for the place-holder-constructor.Does this restrict the type of equation that can be used in a type class? It seems that some equations respecting the constructor discipline are not allowed.I appreciate that in Haskell the most equations occur in the instances, but from my earlier post: I merely wish to identify the strengths and weakness of *current Haskell type classes* as a pure *unit of specification* Is my summarized view is correct?Regards,Pat On 31/07/12, Ryan Ingram ryani.s...@gmail.com wrote:Generally the way this is done in Haskell is that the interface to the type is specified in a typeclass (or, alternatively, in a module export list, for concrete types), and the axioms are specified in a method to be tested in some framework (i.e. QuickCheck, SmallCheck, SmartCheck) which can automatically generate instances of your type and test that the axioms hold.
For example:class QueueLike q where empty :: q a insert :: a - q a - q a viewFirst :: q a - Maybe (a, q a) size :: q a - Integer-- can use a single proxy type if have kind polymorphism, but that's an experimental feature right now
data Proxy2 (q :: * - *) = Proxy2instance Arbitrary (Proxy2 q) where arbitrary = return Proxy2prop_insertIncrementsSize :: forall q. QueueLike q = q () - Boolprop_insertIncrementsSize q = size (insert () q) == size q + 1
prop_emptyQueueIsEmpty :: forall q. QueueLike q = Proxy2 q = Boolprop_emptyQueueIsEmpty Proxy2 = maybe True (const False) $ view (empty :: q ())Then you specialize these properties to your type and test them:
instance QueueLike [] where ...ghci quickCheck (prop_insertIncrementsSize :: [()] - Bool)Valid, passed 100 testsorFailed with: [(), (), ()]QuickCheck randomly generates objects of your data structure and tests your property against them. While not as strong as a proof, programs with 100% quickcheck coverage are *extremely* reliable. SmartCheck is an extension of QuickCheck that tries to reduce test cases to the minimum failing size.
SmallCheck does exhaustive testing on the properties for finite data structures up to a particular size. It's quite useful when you can prove your algorithms 'generalize' after a particular point.
There aren't any libraries that I know of for dependent-type style program proof for haskell; I'm not sure it's possible. The systems I know of have you program in a more strongly typed language (Coq/agda) and export Haskell programs once they are proven safe. Many of these rely on unsafeCoerce in the Haskell code because they have proven stronger properties about the types than Haskell can; I look at that code with some trepidation--I am not sure what guarantees the compiler makes about unsafeCoerce.
-- ryanOn Sun, Jul 22, 2012 at 7:19 AM, Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie wrote:
{-Below is a *specification* of a queue. If possible I would like to write the equations in type class.Does the type class need two type variables? How do I represent the constructors?Can the equations be written in the type class rather than the instance?
-}module QUEUE_SPEC wheredata Queue e = New | Insert (Queue e) e deriving ShowisEmpty :: Queue e - BoolisEmpty New = True isEmpty (Insert q e) = False first :: Queue e - e
first (Insert q e) = if (isEmpty q) then e else (first q) rest :: Queue e - Queue erest (Insert q e ) = if (isEmpty q) then New else (Insert (rest q) e)size :: Queue e - Int
size New = 0 size (Insert q e) = succ (size q){- some tests of above codesize (Insert (Insert (Insert New 5) 6) 3)rest (Insert (Insert (Insert New 5) 6) 3)My first stab at a classclass QUEUE_SPEC q e where
new :: q e insert :: q e - q e isEmpty :: q e - Bool first :: q e - e rest :: q e - q e size :: q e - Int-}
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
[Haskell-cafe] Explaining instance declarations
{- I am trying to understand and provide a *simplified* explanation of instance contexts and their relationship with class hierarchies. I use the example from [1]. Are the following two sentences and annotated code a reasonable explanation? When instantiating an instance I of C, its context must be at the same level or lower than the context of any instance of any super-class of C. The purpose of this rule is to guarantee that the required super-class methods exist. [1] 4.3.2 Instance Declarations http://www.haskell.org/onlinereport/haskell2010/haskellch4.htmlClass hierarchy
Eq1 Show1 Foo
\ / |
\ / |
Num1 Bar
|
|
Num2-}class Foo a whereclass Show1 a whereclass Foo a = Bar a whereclass Eq1 a where-- Eq1 and Show1 are super-classes of Num1 and Num2.class (Eq1 a, Show1 a) = Num1 aclass Num1 a = Num2 a -- We must make an instance of Foo [a], before we can have instance Bar [a]instance (Num1 a) = Foo [a] where -- But that instance of Foo [a] depends on a being a member of Num1-- Hence Bar[a] can only be defined if their exists Num1 a-- But Eq1 Show1 are super classes of Num1-- The following context causes an *error*, because the context is weaker than required-- instance (Eq1 a, Show1 a) = Bar [a] where-- But this is OKinstance (Num1 a) = Bar [a] where-- Also, this would be OK-- instance (Num2 a) = Bar [a] where
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
On 22/07/12, Ertugrul Söylemez e...@ertes.de wrote:You are probably confusing the type class system with something fromOOP. A type class captures a pattern in the way a type is used. Thecorresponding concrete representation of that pattern is then written inthe instance definition: No really. I am investigating the strengths and weaknesses of type classes as a *unit of specification*. I am aware that their primarily intended to act as interface description, which I suppose is a form of specification.To what degree could the QUEUE_SPEC (repeated below) from my first posting be expressed as a type class?From the feedback, I get the impression that an abstract specification such as QUEUE_SPEC cannot be expressed as a type class (as an instance yes).The stumbling block seems to be the abstract representation of constructors.In [1] the classes Moveable and Named are combined, but again each of these classes are pure signatures.Regards,Pat[1]Haskell: The Craft of Functional Programming (Second Edition) Simon Thompson, page 270module QUEUE_SPEC where
data Queue e = New | Insert (Queue e) e deriving Show
isEmpty :: Queue e - Bool
isEmpty New = True
isEmpty (Insert q e) = False
first :: Queue e - e
first (Insert q e) = if (isEmpty q) then e else (first q)
rest :: Queue e - Queue e
rest (Insert q e ) = if (isEmpty q) then New else (Insert (rest q) e)
size :: Queue e - Int
size New = 0
size (Insert q e) = succ (size q)
{-
some tests of above code
size (Insert (Insert (Insert New 5) 6) 3)
rest (Insert (Insert (Insert New 5) 6) 3)
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
Yes. I tried that, but due to my lack of Haskell expertise I cannot write the constructor insertC1 below:
class QUEUE_SPEC_CLASS1 q where
newC1 :: q a
isEmptyC1 :: q a - Bool
insertC1 :: q a - a - q a
sizeC1 :: q a - Int
restC1 :: q a - q a
-- I do not know how to specify constructor insertC1 ?? = ??
insertC1 newC1 a = newC1
isEmptyC1 newC1 = True
-- isEmpty (insertC1 newC1 a) = False On 23/07/12, Alejandro Serrano Mena trup...@gmail.com wrote:I don't know whether this is really applicable but: isn't emptyStack in Ertugrul last message some kind of constructor? You can add any kind of special constructors as functions in the type class which return a new queue. For example:
class Stack s where newEmptyStack :: s a newSingletonStack :: a - s a ...Why doesn't this fulfill you needs of specifying ways to construct new elements?
2012/7/23 Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie
On 22/07/12, Ertugrul Söylemez e...@ertes.de e...@ertes.de wrote:
You are probably confusing the type class system with something fromOOP. A type class captures a pattern in the way a type is used. The
corresponding concrete representation of that pattern is then written inthe instance definition: No really. I am investigating the strengths and weaknesses of type classes as a *unit of specification*.
I am aware that their primarily intended to act as interface description, which I suppose is a form of specification.To what degree could the QUEUE_SPEC (repeated below) from my first posting be expressed as a type class?
>From the feedback, I get the impression that an abstract specification such as QUEUE_SPEC cannot be expressed as a type class (as an instance yes).The stumbling block seems to be the abstract representation of constructors.
In [1] the classes Moveable and Named are combined, but again each of these classes are pure signatures.Regards,Pat[1]Haskell: The Craft of Functional Programming (Second Edition) Simon Thompson, page 270
module QUEUE_SPEC where
data Queue e = New | Insert (Queue e) e deriving Show
isEmpty :: Queue e - Bool
isEmpty New = True
isEmpty (Insert q e) = False
first :: Queue e - e
first (Insert q e) = if (isEmpty q) then e else (first q)
rest :: Queue e - Queue e
rest (Insert q e ) = if (isEmpty q) then New else (Insert (rest q) e)
size :: Queue e - Int
size New = 0
size (Insert q e) = succ (size q)
{-
some tests of above code
size (Insert (Insert (Insert New 5) 6) 3)
rest (Insert (Insert (Insert New 5) 6) 3)
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
Dominique,That is exactly the information that I required.Thank you very much,PatOn 23/07/12, Dominique Devriese dominique.devri...@cs.kuleuven.be wrote:Patrick, -- Class with functional dependency class QUEUE_SPEC_CLASS2 a q | q - a where newC2 :: q a -- ?? sizeC2 :: q a - Int restC2 :: q a - Maybe (q a) insertC2 :: q a - a - q aThe above is a reasonable type class definition for what you seem to intend. -- Without committing to some concrete representation such as list I do not know how to specify constructor for insertC2 ?? = ?? insertC2 newC2 a = newC2 -- wrong isEmptyC2 :: q a - Bool isEmptyC2 newC2 = True -- isEmptyC2 (insertC2 newC2 a) = False wrongCorrect me if I'm wrong, but what I understand you want to do here isspecify axioms on the behaviour of the above interface methods,similar to how the well-known |Monad| class specifies for example m= return === m. You seem to want for example an axiom saying isEmptyC2 newC2 === Trueand similar for possible other equations. With such axioms you don'tneed access to actual constructors and you don't want access to thembecause concrete implementations may use a different representationthat does not use such constructors. Anyway, in current Haskell, suchtype class axioms can not be formally specified or proven but they aretypically formulated as part of the documentation of a type class andimplementations of the type class are required to satisfy them butthis is not automatically verified.Dominique Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] specifying using type class
{-Below is a *specification* of a queue. If possible I would like to write the equations in type class.Does the type class need two type variables? How do I represent the constructors?Can the equations be written in the type class rather than the instance?-}module QUEUE_SPEC wheredata Queue e = New | Insert (Queue e) e deriving ShowisEmpty :: Queue e - BoolisEmpty New = True isEmpty (Insert q e) = False first :: Queue e - efirst (Insert q e) = if (isEmpty q) then e else (first q) rest :: Queue e - Queue erest (Insert q e ) = if (isEmpty q) then New else (Insert (rest q) e)size :: Queue e - Intsize New = 0 size (Insert q e) = succ (size q){- some tests of above codesize (Insert (Insert (Insert New 5) 6) 3)rest (Insert (Insert (Insert New 5) 6) 3)My first stab at a classclass QUEUE_SPEC q e where new :: q e insert :: q e - q e isEmpty :: q e - Bool first :: q e - e rest :: q e - q e size :: q e - Int-}
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] specifying using type class
Ertugrul ,Thanks for you very clear explanation.Without committing to some concrete representation such as list I do
not know how to specify constructors in the class (see below). As you point out a class may not be appropriate for an actual application, but I am investigating the strengths and weaknesses of class as a unit of *specification*.Regards,Pat-- Class with functional dependencyclass QUEUE_SPEC_CLASS2 a q | q - a where newC2 :: q a -- ?? sizeC2 :: q a - Int restC2 :: q a - Maybe (q a) insertC2 :: q a - a - q a-- Without committing to some concrete representation such as list I do not know how to specify constructor for insertC2 ?? = ?? insertC2 newC2 a = newC2 -- wrong isEmptyC2 :: q a - Bool isEmptyC2 newC2 = True-- isEmptyC2 (insertC2 newC2 a) = False wrongOn 22/07/12, Ertugrul Söylemez e...@ertes.de wrote:Patrick Browne patrick.bro...@dit.ie wrote: {- Below is a *specification* of a queue. If possible I would like to write the equations in type class. Does the type class need two type variables? How do I represent the constructors? Can the equations be written in the type class rather than the instance? -}(Side note: When opening a new topic, please don't /reply/ to a post,but post it separately by creating a new mail.)The type class needs to know the element type, so your observation iscorrect. Usually, as in your case, the element type follows from thedata structure type, and you will want to inform the type system aboutthis connection. There are basically three ways to do it. The first isusing MultiParamTypeClasses and FunctionalDependencies: class Stacklike a s | s - a where empty :: s a null :: s a - Bool push :: a - s a - s a pop :: s a - Maybe a size :: s a - Int tail :: s a - Maybe (s a)Another way is using an associated type (TypeFamilies). This iscleaner, but much more noisy in the type signatures: class Stacklike s where type StackElement s empty :: s (StackElement s) null :: s (StackElement s) - Bool push :: StackElement s - s (StackElement s) - s (StackElement s) pop :: s (StackElement s) - Maybe (StackElement s) size :: s (StackElement s) - Int tail :: s (StackElement s) - Maybe (s (StackElement s))Finally once you realize that there is really no need to fix the elementtype in the type class itself, you can simply write a type class for thetype constructor, similar to how classes like Functor are defined: class Stacklike s where empty :: s a null :: s a - Bool push :: a - s a - s a pop :: s a - Maybe a size :: s a - Int tail :: s a - Maybe (s a)The big question is whether you want to write a class at all. Usuallyclasses are used to capture patterns, not operations.Greets,Ertugrul-- Not to be or to be and (not to be or to be and (not to be or to be and(not to be or to be and ... that is the list monad.
Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] overloading
Hi,I am comparing Haskell's class/instance techniques for overloading with those available Order Sorted Algebra (OSA in CafeOBJ) Using just the basic class/instance mechanism is there any way to avoid the type annotations in the evaluations below?Patclass Location a b where move::a-binstance Location Int Int where move e = e + 3instance Location Float Int where move e = floor(e + 3.1) instance Location [Float] [Int] where move [] = [] move (e:l) = (move e):(move l)instance Location [Int] [Int] where move [] = [] move (e:l) = (move e):(move l)-- evaluations-- testing float-- (move ((7.6::Float))::Int)-- ((move ([21.8,7.4,9.1]::[Float]))::[Int])-- testing integers-- move ((3::Int))::Int-- ((move ([21,7,9]::[Int]))::[Int]) Tá an teachtaireacht seo scanta ó thaobh ábhar agus víreas ag Seirbhís Scanta Ríomhphost de chuid Seirbhísí Faisnéise, ITBÁC agus meastar í a bheith slán. http://www.dit.ie 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Theorems for free!
Hi, I apologize if the formatting or content of my previous email caused offence. Hopefully my question is better phrased and presented this time. Below is my attempt to code the first example from Walder’s Theorems for free! paper[1]. {-# LANGUAGE ExistentialQuantification #-} import Data.Char r :: forall a . [a] - [a] r = reverse g :: Char - Int g = ord (map g . r $ ['a','b','c']) == (r . map g $ ['a','b','c']) I am not sure about what is being proved. Wadler says: It is possible to conclude that r satisifies the following theorem r must work on lists of X for any types X. So does evaluation demonstrate type level satisfiability? Thanks, Pat [1] homepages.inf.ed.ac.uk/wadler/papers/free/free.ps
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Theorems for free!
Hi,
Below is my attempt to code the first example from Walder’s Theorems for
free! paper.
I am not sure about what is being proved.
Using the notation from the paper does the proof establish a
property of map, r, composition or the relationship between all three?
{-# LANGUAGE ExistentialQuantification #-}
import Data.Char
r :: forall a . [a] - [a]
r = reverse
g :: Char - Int
g = ord
(map g . r $ ['a','b','c']) == (r . map g $ ['a','b','c'])
Regards,
Pat
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Theorems for free!
Wojciech,
I apreciate that the example only satisifies rather than
proves the theorem.
Wadler
says “it is possible to conclude that r satisifies the following theorem”
r must work on lists of X for any types
X.
So does evaluation demonstrate type
level satisfiability?
Thanks,
Pat
On 27/02/12, Wojciech Jedynak wjedy...@gmail.com wrote:Hello Patrick.I've read the paper just a few days ago and that particular examplewas presented to show the general idea in a concrete setting - nothingmore. The general idea here is that if r is a polymorphic function onlists, then it doesn't matter whether you apply the map functionbefore or after applying the r itself.Hope that helps,Wojciech2012/2/27 Patrick Browne patrick.bro...@dit.ie: Hi, Below is my attempt to code the first example from Walder’s Theorems for free! paper. I am not sure about what is being proved. Using the notation from the paper does the proof establish a property of map, r, composition or the relationship between all three? {-# LANGUAGE ExistentialQuantification #-} import Data.Char r :: forall a . [a] - [a] r = reverse g :: Char - Int g = ord (map g . r $ ['a','b','c']) == (r . map g $ ['a','b','c']) Regards, Pat ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The Riddle of the Buddhist Monk
Sameer, I think that my Maude to Haskell translation was a bit too literal and naive. But your reply helped me gain further insight to both languages, which is essentially my current research task. Thanks, Pat On 12/23/11, Sameer Sundresh sam...@sundresh.org wrote:On Wed, Dec 21, 2011 at 10:12 AM, Patrick Browne patrick.bro...@dit.ie patrick.bro...@dit.ie wrote: On 21/12/11, Richard O'Keefe o...@cs.otago.ac.nz o...@cs.otago.ac.nz 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 = Timeu2I'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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The Riddle of the Buddhist Monk
On 21/12/11, Richard O'Keefe o...@cs.otago.ac.nz 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. 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 [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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] The Riddle of the Buddhist Monk
Hi,I am trying to implement a set of 4 modules that blend the action of a monk moving up a mountain on day 1 and returning down by the same path on day 2 [1][2]. The code should reflect the fact that there is some time and place which is common to the two days where the monk would *meets himself*. My Haskell code is based on a Maude version[3][4]. Only 3 times and places are considered in the code; start, meet, and end called 1,2, and 3 (e.g. the start time for the upward journey is timeu1).Using qualified elements, I can get the meets function to give the correct results, but I cannot get the location function to work.Is it possible the get meets to work without qualification? Any suggestions in getting location to work?Regards,Pat -- *** MODULE 1module MONKONMOVE wheredata Monk = Monk String deriving (Eq,Show)data TimeOfDay = TimeOfDay String deriving (Eq,Show)data LocationOnPath = LocationOnPath String deriving (Eq,Show)meets :: Monk - Monk - TimeOfDay - TimeOfDay - LocationOnPath - LocationOnPath - Boolmeets m1 m2 t1 t2 l1 l2 = if (not(m1 == m2) (t1 == t2) (l1 == l2)) then True else False-- I am not sure that I actually need a type class, I just put it here to stop compiler errors.class LOCATION m t l where location :: m - t - l -- *** MODULE 2module MONKONMOVEUP whereimport MONKONMOVEmonku :: Monkmonku = Monk munkutimeu1 :: TimeOfDaytimeu1 = TimeOfDay timeu1timeu2 :: TimeOfDaytimeu2 = TimeOfDay timeu2timeu3 :: TimeOfDaytimeu3 = TimeOfDay timeu3locationu1 :: LocationOnPathlocationu1 = LocationOnPath locationu1locationu2 :: LocationOnPathlocationu2 = LocationOnPath locationu2locationu3 :: LocationOnPathlocationu3 = LocationOnPath locationu3instance LOCATION Monk TimeOfDay LocationOnPath where location monku timeu1 = locationu1 location monku timeu2 = locationu2 location monku timeu3 = locationu3 -- *** MODULE 3module MONKONMOVEDOWN whereimport MONKONMOVEmonkd :: Monkmonkd = Monk munkdtimed1 :: TimeOfDaytimed1 = TimeOfDay timed1timed2 :: TimeOfDaytimed2 = TimeOfDay timed2timed3 :: TimeOfDaytimed3 = TimeOfDay timeu3locationd1 :: LocationOnPathlocationd1 = LocationOnPath locationd3locationd2 :: LocationOnPathlocationd2 = LocationOnPath locationd2locationd3 :: LocationOnPathlocationd3 = LocationOnPath locationd1instance LOCATION Monk TimeOfDay LocationOnPath where location monkd timed1 = locationd3 location monkd timed2 = locationd2 location monkd timed3 = locationd1 -- *** MODULE 4module MONKMEETSHIMSELF whereimport MONKONMOVEUP import MONKONMOVEDOWN-- There is one time and location in commonlocationd2 = locationu2timed2 = timeu2-- The start of one journey is the end of the other and visa versalocationd1 = locationu3locationd3 = locationu1timed1 = timeu1timed3 = timeu3 -- The following are executable in MONKMEETSHIMSELF, but all the elements must be qualified their module name.meets monku monkd timeu2 timed2 locationu2 locationd2 -- truemeets monku monkd timeu2 timed2 locationu2 locationd3 -- false-- For exampleMONKONMOVE.meets monku monkd MONKONMOVEUP.timeu2 MONKMEETSHIMSELF.timed2 MONKONMOVEUP.locationu2 MONKMEETSHIMSELF.locationd2 -- I cannot get the location function to work in MONKMEETSHIMSELFlocation monku timeu2 == location monkd timed2 – should be truelocation monkd timed2 -- should be locationd2 [1] http://markturner.org/blending.html[2] http://cseweb.ucsd.edu/~goguen/pps/taspm.pdf[3] http://lists.cs.uiuc.edu/pipermail/maude-help/2010-December/000456.html[4] http://lists.cs.uiuc.edu/pipermail/maude-help/2010-December/000462.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The Riddle of the Buddhist Monk
On 12/20/11, Paul Johnson p...@cogito.org.uk wrote:I think you need to rethink the solution: Haskell is not a logic programming language. Yes of course, but I suspect that the problems are due to issues of scope and modularity rather than problems of a logical nature The main equation for meets does give the appropriate results. Pat ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The Riddle of the Buddhist Monk
On 12/20/11, Paul Johnson p...@cogito.org.uk wrote:You definitely don't need the type class, and you don't need instances.I have removed the type class and instances.I have placed the location function in MONKONMOVEUP and MONKONMOVEDOWNNow I can at least access the functions and some of values. For exampleMONKMEETSHIMSELF.timeu1interactive:1:1: Not in scope: `MONKMEETSHIMSELF.timeu1'MONKMEETSHIMSELF.timed1TimeOfDay timeu1 Is there any set of imports or exports that could make the modules work together in a consistent way? Thanks,Pat -- *** MODULE 1 module MONKONMOVE where data Monk = Monk String deriving (Eq,Show) data TimeOfDay = TimeOfDay String deriving (Eq,Show) data LocationOnPath = LocationOnPath String deriving (Eq,Show) meets :: Monk - Monk - TimeOfDay - TimeOfDay - LocationOnPath - LocationOnPath - Bool meets m1 m2 t1 t2 l1 l2 = if (not(m1 == m2) (t1 == t2) (l1 == l2)) then True else False -- *** MODULE 2 module MONKONMOVEUP where import MONKONMOVE monku :: Monk monku = Monk munku timeu1 :: TimeOfDay timeu1 = TimeOfDay timeu1 timeu2 :: TimeOfDay timeu2 = TimeOfDay timeu2 timeu3 :: TimeOfDay timeu3 = TimeOfDay timeu3 locationu1 :: LocationOnPath locationu1 = LocationOnPath locationu1 locationu2 :: LocationOnPath locationu2 = LocationOnPath locationu2 locationu3 :: LocationOnPath locationu3 = LocationOnPath locationu3 location :: Monk - TimeOfDay - LocationOnPathlocation monku timeu1 = locationu1 location monku timeu2 = locationu2location monku timeu3 = locationu3 -- *** MODULE 3 module MONKONMOVEDOWN where import MONKONMOVE monkd :: Monk monkd = Monk munkd timed1 :: TimeOfDay timed1 = TimeOfDay timed1 timed2 :: TimeOfDay timed2 = TimeOfDay timed2 timed3 :: TimeOfDay timed3 = TimeOfDay timeu3 locationd1 :: LocationOnPath locationd1 = LocationOnPath locationd3 locationd2 :: LocationOnPath locationd2 = LocationOnPath locationd2 locationd3 :: LocationOnPath locationd3 = LocationOnPath locationd1 location :: Monk - TimeOfDay - LocationOnPath location monkd timed1 = locationd3location monkd timed2 = locationd2 location monkd timed3 = locationd1 -- *** MODULE 4 module MONKMEETSHIMSELF where import MONKONMOVEUP import MONKONMOVEDOWN -- There is one time and location in common locationd2 = locationu2 timed2 = timeu2 -- The start of one journey is the end of the other and visa versa locationd1 = locationu3 locationd3 = locationu1 timed1 = timeu1 timed3 = timeu3 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The Riddle of the Buddhist Monk
I have simplified the code using constructors and export.I can evalute the qualified expressions but I do not get the expected results.module MONKONMOVE (module MONKONMOVE)wheredata Monk = Monk | Monku | Monkd deriving (Show,Eq)data TimeOfDay = TimeOfDay | Timeu1 | Timeu2 | Timeu3 | Timed1 | Timed2 | Timed3 deriving (Show,Eq)data LocationOnPath = LocationOnPath | Locationu1 | Locationu2 | Locationu3 | Locationd1 | Locationd2 | Locationd3 deriving (Show,Eq)meets :: Monk - Monk - TimeOfDay - TimeOfDay - LocationOnPath - LocationOnPath - Bool meets m1 m2 t1 t2 l1 l2 = if (not(m1 == m2) (t1 == t2) (l1 == l2)) then True else Falsemodule MONKONMOVEUP (module MONKONMOVE,module MONKONMOVEUP) whereimport MONKONMOVE location :: Monk - TimeOfDay - LocationOnPathlocation Monku Timeu1 = Locationu1location Monku Timeu2 = Locationu2location Monku Timeu3 = Locationu3module MONKONMOVEDOWN (module MONKONMOVE, module MONKONMOVEDOWN) whereimport MONKONMOVElocation :: Monk - TimeOfDay - LocationOnPathlocation Monkd Timed1 = Locationd3location Monkd Timed2 = Locationd2location Monkd Timed3 = Locationd1module MONKMEETSHIMSELF whereimport MONKONMOVEUP import MONKONMOVEDOWN -- There is one time and location in commonLocationu2 = Locationd2 Timed2 = Timeu2 -- The start of one journey is the end of the other and vice versaLocationd1 = Locationu3 Locationd3 = Locationu1 Timed1 = Timeu1 Timed3 = Timeu3 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Do type classes have a partial order?
Is there a partial order on Haskell type classes?If so, does it induce any quasi-order relation on types named in the instances?In the example below types C and D have the same operation fThanks,Patdata C = C deriving Showdata D = D deriving Showclass A t where f::t-t f t = t instance A C whereinstance A D whereclass A t = B t whereinstance B C whereinstance B D where ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Haskell V Java type checking
Hi,I am comparing some aspects of Haskell with Java.Below is a simple Haskell program with a sub-class.It is followed my attempt to code the same concepts in Java.Two questions:1) Are the two examples close enough? (very subjective)2) In this example, what are the advantages of the Haskell type checking over the Java type checking? 3) Are there more general advantages of Haskell type checking over Java type checking?Regards,Pat Haskell program===data Cdata Dclass A t whereinstance A C whereinstance A D whereclass A t = B t whereinstance B C whereinstance B D where=Java Program===import java.lang.Class;interface AT {}class A_INSTANCET implements AT {}interface BT extends AT{}class B_INSTANCET implements BT {}class C {}class D {}public class DEMO1 {public static void main(String args[]) {A_INSTANCEC ac = new A_INSTANCEC();A_INSTANCED ad = new A_INSTANCED();B_INSTANCEC bc = new B_INSTANCEC();B_INSTANCED bd = new B_INSTANCED();System.out.println(Object's Class name =+ ac.getClass().getName());System.out.println(Object's Class name =+ ad.getClass().getName());System.out.println(Object's Class name =+ bc.getClass().getName());System.out.println(Object's Class name =+ bd.getClass().getName()); }}
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] subclasses and classes with same type in instance
Hi,Does the subclass relation have any meaning when two classes have instances with the same type?I get the same results from Listing 1 and Listing 2 below.Regards,Pat-- Listing 1- Subclassdata Shed = Shed class Building building where addressB :: building - Integer addressB b = 1-- subclass, but none in Listing 2class Building house = House house where addressH :: house - Integer addressH b = 0instance Building Shed whereinstance House Shed where-- Listing 2 -- No subclassdata Shed = Shed class Building building where addressB :: building - Integer addressB b = 1-- No subclass class Building house = House house where addressH :: house - Integer addressH b = 0instance Building Shed whereinstance House Shed where-- Test runs give same result for Listing 1 and Listing 2-- addressH Shed-- addressB Shed ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Correction: subclasses and classes with same type in instance
Hi, Does the subclass relation have any meaning when two classes have instances with the same type? I get the same results from Listing 1 and Listing 2 below. Regards, Pat -- Listing 1- Subclass data Shed = Shed class Building building where addressB :: building - Integer addressB b = 1 -- subclass, but none in Listing 2 class Building house = House house where addressH :: house - Integer addressH b = 0 instance Building Shed where instance House Shed where -- Listing 2 -- No subclass data Shed = Shed class Building building where addressB :: building - Integer addressB b = 1 -- No subclass class House house where addressH :: house - Integer addressH b = 0 instance Building Shed where instance House Shed where -- Test runs give same result for Listing 1 and Listing 2 -- addressH Shed -- addressB Shed ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Correction: subclasses and classes with same type in instance
In the current example does the following totally or partially ignore the type class system.boo :: Shed - Integerboo h = addressB h + addressH hOn 16/10/11, Daniel Fischer daniel.is.fisc...@googlemail.com wrote:In your example, the only difference is that with the superclass constraintfoo :: House h = h - Integerfoo h = addressB h + addressH hworks, while without superclass constraint, foo would need both classes in its context. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Overloading in a sub-class
Hi, Below are two questions concerning overloading in a sub-class. Thanks, Pat class Numb0 a where (+) :: a - a - a negate :: a - a instance Numb0 Int where x + y = y negate x = x -- Are + and negate part of the signature of Numb1? class Numb0 a = Numb1 a where -- Is it possible to override these operations in instances of Numb1? -- Something like: -- instance Numb1 Float where --x + y = y --negate x = x -- Or even using Int as in the super class instance: -- instance Numb1 Int where --x + y = y --negate x = x 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type-class inference
The :info command is a great help. Why does :info g 4 produce a parse error, while :t g 4 does not? Thanks for all your help, Pat On 13/08/2011 00:08, Brandon Allbery wrote: Typeclasses are not independent of types, and are not inferred separately from types. If you want to know what typeclasses a type is a member of, use :info. On 12/08/2011 23:52, Patrick Browne wrote: Hi, Why does the Haskell :type command only sometimes print the type-class? Should I expect type-class inference as well as type inference? Maybe the type-class is inferred where possible, but not always printed? Thanks, Pat -- Code k x = x + 3 data T = T class A a where g::a - a g a = a instance A T where instance A Integer where -- The results from the above code. -- First in the case of a function. Inferred the Num class *Main :t k k :: forall a. (Num a) = a - a *Main :t k 3 k 3 :: forall t. (Num t) = t -- Did not print type class *Main :t k (3::Integer) k (3::Integer) :: Integer -- Second in the case of a method of a type class. -- Inferred Num *Main :t g 3 g 3 :: forall t. (A t, Num t) = t -- Did not print class A. *Main :t g T g T :: T -- Did not print any class. *Main :t g (3::Integer) g (3::Integer) :: Integer 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] type-class inference
Hi, Why does the Haskell :type command only sometimes print the type-class? Should I expect type-class inference as well as type inference? Maybe the type-class is inferred where possible, but not always printed? Thanks, Pat -- Code k x = x + 3 data T = T class A a where g::a - a g a = a instance A T where instance A Integer where -- The results from the above code. -- First in the case of a function. Inferred the Num class *Main :t k k :: forall a. (Num a) = a - a *Main :t k 3 k 3 :: forall t. (Num t) = t -- Did not print type class *Main :t k (3::Integer) k (3::Integer) :: Integer -- Second in the case of a method of a type class. -- Inferred Num *Main :t g 3 g 3 :: forall t. (A t, Num t) = t -- Did not print class A. *Main :t g T g T :: T -- Did not print any class. *Main :t g (3::Integer) g (3::Integer) :: Integer 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Difference between class and instance contexts
Below are examples of using the sub-class context at class level and at instance level. In this simple case they seem to give the same resultsIn general, are there certain situations in which one or the other is preferred? Patmodule CLASS where-- class and sub-classclass Class a where foo :: a - a foo a = aclass Class a = SubClass a where moo :: a - a moo a = foo ainstance Class Integer whereinstance SubClass Integer where*CLASS :t foo 2foo 2 :: forall t. (Class t, Num t) = t*CLASS :t moo 2moo 2 :: forall t. (SubClass t, Num t) = tmodule INSTANCE where-- Using context at instance level-- Is class Class a where foo :: a - a foo a = aclass SubClass a where moo :: a - ainstance Class Integer whereinstance Class Integer = SubClass Integer where moo a = foo aINSTANCE :t foo 2foo 2 :: forall t. (Class t, Num t) = tINSTANCE :t moo 2moo 2 :: forall t. (SubClass t, Num t) = t ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] difference between class context and deriving
What is the difference between using a class context and deriving in data type declaration? Are there certain situations in which one or the other is preferred? data Eq a = Set1 a = NilSet1 | ConsSet1 a (Set1 a) data Set2 a = NilSet2 | ConsSet2 a (Set2 a) deriving Eq (NilSet1) == (NilSet1) -- no instance, error (NilSet2) == (NilSet2) -- True -- seems OK type Type1 = Set1 Integer type Type2 = Set2 Integer -- seems OK data Data1 = Set1 | Set2 -- Seems to have same type :t ConsSet2 1 NilSet2 ConsSet2 1 NilSet2 :: forall t. (Num t) = Set2 t :t ConsSet1 1 NilSet1 ConsSet1 1 NilSet1 :: forall t. (Num t) = Set1 t -- 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] logic and types
Hi, Below are some questions about the logical interpretation of types and type classes. Thanks, Pat module J where type Id = String type Position = Integer data Person = Person Id Position deriving Show -- Is this an axiom at type level? class Pos a where getPos :: a - Position -- The :type command says -- forall a. (Pos a) = a - Position -- How do I write this in logic? (e.g. implies, and, or, etc) -- What exactly is being asserted about the type variable and/or about the class? -- I am not sure of the respective roles of = and - in a logical context -- Is the following a fact at type level, class level or both? instance Pos Person where getPos (Person i p) = p -- Is it the evaluation or the type checking that provides a proof of type correctness? -- getPos(Person 1 2) 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Introspection
Is it possible to access type information and perform either of the following in a Haskell program? 1) Find the type/class of a variable e.g. a type predicate: is y of-type A, or is y of-Class A 2) Assert the type of a variable e.g. if y.length 100 then y is of type big. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Introspection
On 22/07/2011 10:18, Patrick Browne should have wrote: 2) Assert the class of a variable e.g. if y.length 100 then y is of class big. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] partial inheritance
On 18/07/2011 13:52, Ketil Malde wrote: I'm not sure the question makes sense, if fly is a method of class Bird, then it can't also be a member of class Penguin. I am actually doing a language comparison and I was checking out a paper that said: Type classes allow for partial inheritance, so that penguins can be birds without flying behavior. My question is concerned with the language constructs to do this rather than the semantic validity or desirability of such construct. But as pointed out by Jerzy my question is silly because can penguins can fly: On 17/07/2011 11:14, Jerzy Karczmarczuk wrote: PS. Penguins DO fly. http://www.telegraph.co.uk/news/worldnews/1583517/Flying-penguins-found-by-BBC-programme.html 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] partial inheritance
On 18/07/2011 19:14, Jerzy Karczmarczuk wrote: That's why I suggested how you might do that: for some datatypes, say the Emperors, you specify some special flying method (e.g. dummy or bombing), or you don't specify it at all. And the Emperors won't fly. -- Here is my attempt data Emperor = Emperor data Robin = Robin class Bird a where fly :: a - a - a walk :: a - a - a instance Bird Robin where fly x y = y walk x y = x instance Bird Emperor where -- No fly method walk x y = y class (Bird a) = Penguin a where -- I do not think that I can override the walk method in the sub-class -- must be done in instance of Penguin instance Penguin Emperor where -- How can I override the walk method in the instance Penguin? -- walk x y = x 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Constructor discipline and dependent types.
Hi, My understanding of the constructor discipline (CD) is that it is a restriction on the form of an equation that guarantees that the equation represents an executable function. The CD restricts the LHS of an equation to consist of a function name, constructors, and variables. Also there should be no new variables on the RHS. So CD permits function to be defined and prohibits general assertions which are more in the domain of a specification language. Question 1: Is the above a reasonable understanding of CD? Question 2: I have read that the lack of dependent types (DT) prevents writing general assertions in Haskell. Is CD related to DT? If so how are they related? 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] partial inheritance
Hi, Is it possible to model partial inheritance using Haskell type classes? For example, if the class Bird has a flying method can we represent Penguins as a sub-class of Bird without a flying method? 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] class and instance
Hi, I am trying to understand the following code. I have written my current (mis-)understanding and questions below. I do not wish to improve the code, it is from a research paper[1] that I am trying to understand. Pat [1] ftp://ftp.geoinfo.tuwien.ac.at/medak/phdmedak.pdf -- A specification. The class Points takes two type variables. -- The functions take variables of type p, a; return a value of type a. class Points p a where getX :: p a - a getY :: p a - a -- A parameterized representation -- One constructor takes two elements of type a and produces a Point. data Point a = Pt a a -- An implementation of the class Points on the data type (Point a) -- In Pt b c constructor the variables b and c areboth of type a. -- The type a is left undefined until evaluation instance Points Point a where getX (Pt b c) = b getY (Pt b c) = c -- This runs with any type e.g. Integers -- getX(Pt 1 2) -- :t getX(Pt 1 2) -- getX(Pt 1 2) :: forall t. (Num t) = t My main question is in understanding the relationship between the arguments of the functions getX and getY in the class and in the instance. It seems to me that the constructor Pt 1 2 produces one element of type Point which has two components. How does this square with the class definition of getX which has two arguments? Is there a difference between: getX :: p a - a and getX :: p - a - a 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Instances and multiple inheritance
How do I make an instance of the Vehicles class below? Thanks, Pat class Containers x y where insert :: y - x y - x y remove :: y - x y - x y whatsIn :: x y - [y] instance Containers [] Char where insert y [] = y:[] insert y m = y:m remove _ [] = [] remove x (y:ys) | x == y= remove x ys | otherwise = y : remove x ys whatsIn = id instance Containers [] Integer where insert y [] = y:[] insert y m = y:m remove _ [] = [] remove x (y:ys) | x == y= remove x ys | otherwise = y : remove x ys whatsIn = id instance Containers [] [a] where insert x y = x:y -- lists of lists -- insert [1] [[3,6],[45]] class Surfaces a b where put :: b - a b - a b takeOff :: b - a b - a b whatsOn :: a b - [b] instance Surfaces [] Integer where put y [] = y:[] put y m = y:m takeOff _ [] = [] takeOff x (y:ys) | x == y= takeOff x ys | otherwise = y : takeOff x ys whatsOn = id class Contacts a b where attach :: b - a b - a b detach :: b - a b - a b whatsAt :: a b - [b] instance Contacts [] Integer where attach y [] = y:[] attach y m = y:m detach _ [] = [] detach x (y:ys) | x == y= detach x ys | otherwise = y : takeOff x ys whatsAt = id class Paths a b c where move :: c - a b c - a b c origin, destination :: a b c - b whereIs :: a b c - c - b instance Paths (,) Integer Integer where -- `Integer - (Integer, Integer) - (Integer, Integer)' move c (a,b) = (a+1,b+1) origin (a,b) = a destination (a,b) = b whereIs (a, b) c = b -- Test -- move (1::Integer) (3::Integer,5::Integer) -- origin (3::Integer,5::Integer) class People p where class HeavyLoads l where class Surfaces w o = WaterBodies w o where instance WaterBodies [] Integer where class Containers h o = Houses h o where class (Surfaces v o, Paths a b (v o)) = Vehicles v o a b where -- I do not know how to make an instance of Vehicles -- What seems to be the *obvious* does not work -- instance Vehicles [] Integer (,) Integer Integer where -- Kind error: `Vehicles' is applied to too many type arguments -- In the instance declaration for -- `Vehicles [] Integer (,) Integer Integer' 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Instances and multiple inheritance
On 12/06/2011 10:43, MigMit wrote: I fail to understand why instantiating a four-argument class with five arguments seems obvious to you. class (Surfaces v o, Paths a b (v o)) = Vehicles v o a b where Obviously I am wrong! But my incorrect thinking is as follows: Surfaces takes 2 arguments, Paths take 3 arguments (giving 5). I do not know how to group those 5 arguments to make the required 4 for Vehicles. The original classes were defined in [1]. Thanks, Pat [1] Modeling the Semantics of Geographic Categories through Conceptual Integration (2002) by Werner Kuhn http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.109.6853 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Class and Instance
Thanks for the feedback. I have two further questions 1. Why is it that the Containers class signature does not allow instances to be list of list? I suspect it is because x is a constructor. 2. How would I change the Containers class signature to allow instances to be lists of lists. Thanks, Pat -- x is a type constructor, not a type class Containers x y where insert :: y - x y - x y remove :: y - x y - x y whatsIn :: x y - [y] instance Containers [] Char where insert y [] = y:[] insert y m = y:m remove _ [] = [] remove x (y:ys) | x == y= remove x ys | otherwise = y : remove x ys whatsIn = id instance Containers [] Integer where insert y [] = y:[] insert y m = y:m remove _ [] = [] remove x (y:ys) | x == y= remove x ys | otherwise = y : remove x ys whatsIn = id -- cannot have containers of containers. -- instance Containers [] [] where -- container.hs:41:23: --`[]' is not applied to enough type arguments -- Expected kind `*', but `[]' has kind `* - *' -- In the instance declaration for `Containers [] []' -- Failed, modules loaded: none. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Class and Instance
Hi Below is a class that I wish to create some instances of. I do not wish to change the class definition. It is supposed to represent containers of type x that contain things of type y. My attempt at the insert function seems ok for Char and lists, but not ok for Integer. How do I instantiate this class for integers and lists? Does this class definition permit y to be a list and hence x to be a list of lists? Something like: instance Containers [] [] where .. Is this a constructor class? Thanks, Pat class Containers x y where insert :: y - x y - x y remove :: y - x y - x y whatsIn :: x y - [y] instance Containers [] Char where insert y [] = y:[] insert y m = y:m instance Containers [] Integer where insert y [] = y:[] insert y m = y:m -- OK -- insert '1' ['u','u','l','i'] -- Not OK -- insert 2 [9,2] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Are casts required?
Are casts required to run the code below? If so why? Thanks, Pat -- Idetifiers for objects class (Integral i) = IDs i where startId :: i newId :: i - i newId i = succ i sameId, notSameId :: i - i - Bool -- Assertion is not easily expressible in Haskell -- notSameId i newId i = True sameId i j = i == j notSameId i j = not (sameId i j) startId = 1 instance IDs Integer where -- are casts need here? sameId (newId startId::Integer) 3 sameId (3::Integer) (4::Integer) notSameId (3::Integer) (newId (3::Integer)) 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] lambda abstraction
Are the following two functions equivalent? (i.e. do they describe the same computation) let add1 a = a + 2 let add2 = \ a - a + 2 :t add1 add1 :: forall a. (Num a) = a - a :t add2 add2 :: forall a. (Num a) = a - a Does Haskell interpreter convert all functions in the form of add1 to the lambda form of add2? Does this lambda form represent the operational semantics of Haskell? How should I translate the type information into English? Thanks 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Sub class and model expansion
Continuing the thread on model expansion. I have changed the example trying to focus on expanding models of M in G Why is the operation ! ok or RHS but not visible on LHS of G? The equation itself does not seem to suffer from the dependent type problem of my previous post. class M a where (!) :: a - a - a e :: a class M a = G a where (!-) :: a - a - a -- OK in G a !- e = e ! a -- Switching LHS/RHS is not OK in G but fine in S -- if I declare both ! and !- in S -- ! is not a (visible) method of class `G' -- a ! e = e !- a Thanks, Pat On 30/05/2011 00:47, Brandon Moore wrote: From: Patrick Brown; Sent: Sunday, May 29, 2011 5:42 PM Subject: Re: [Haskell-cafe] Sub class and model expansion Ryan, Thank you for your helpful reply. I have no real understanding of dependent types (DT) From the web is seems that DTs are types that depend on *values*. How does the concept of DT relate to the equation from my example? -- inverse a ! a = e What type is depending on what value? You want part of the group interface to be a proof that your inverse function agrees property with the monoid operation and unit. If that's going to be a value, it has to have some type. If that type is anything like Proof that inverse a ! a = e, then the type mentions, or depends on the values inverse, (!), and e. You can see exactly this in the Agda standard library, in the definitions IsMonoid and IsGroup in Algebra.Structures, which define records containing proofs that a set of operations actually forms a monoid or group. You could probably avoid the apparent circularity of full dependent types if you split up a language into values which can have types, and a separate pair of propositions and proofs which can refer to values and types, but not to themselves. I think that's basically the organization of any system where you use a separate prover to prove things about programs in some previously-existing programming language, but I haven't stumbled across any examples where that sort of organization was designed into a single language from the start. Brandon 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Sub class and model expansion
Ryan, Thank you for your helpful reply. I have no real understanding of dependent types (DT) From the web is seems that DTs are types that depend on *values*. How does the concept of DT relate to the equation from my example? -- inverse a ! a = e What type is depending on what value? Once again thanks for time and insight. Pat On 29/05/2011 22:45, Ryan Ingram wrote: Hi Patrick. What you are doing isn't possible in source code (Haskell doesn't prove things at the value level like a dependently typed language does.) Usually you document it just as you have, as a comment -- inverse a ! a = e You can also specify a QuickCheck property: propInverse :: (Eq a, Group a) = a - Bool propInverse a = (inverse a ! a) == e I've put up an example on hpaste at http://hpaste.org/47234/simple_monoid -- ryan On Sat, May 28, 2011 at 2:46 AM, Patrick Browne patrick.bro...@dit.ie mailto:patrick.bro...@dit.ie wrote: Hi, I'm not sure if this is possible but I am trying to use Haskell’s type class to specify *model expansion*. Model expansion allows the specification of new symbols (known as enrichment) or the specification further properties that should hold on old symbols. I am trying to enrich simplified Monoids to Groups. The code below is not intended to do anything other than to specify simplified Groups as a subclass of Monoid. The main problem is that I cannot use ! on the LHS of equations in Group. Is it possible to expand the specification of Monoid to Group using Haskell type classes? Pat data M = M deriving Show -- Monoid with one operation (!) and identity e (no associativity) class Monoid a where (!) :: a - a - a e :: a a ! e = a -- A Group is a Monoid with an inverse, every Group is a Monoid -- (a necessary condition in logic: Group implies Monoid) -- The inverse property could be expressed as: -- 1) forAll a thereExists b such that a ! b = e -- 2) (inv a) ! a = e class Monoid a = Group a where inverse :: a - a -- Haskell does not like ! on the LHS of equation for inverse in Group. -- (inverse a) ! a = e 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org mailto:Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Sub class and model expansion
Hi, I'm not sure if this is possible but I am trying to use Haskell’s type class to specify *model expansion*. Model expansion allows the specification of new symbols (known as enrichment) or the specification further properties that should hold on old symbols. I am trying to enrich simplified Monoids to Groups. The code below is not intended to do anything other than to specify simplified Groups as a subclass of Monoid. The main problem is that I cannot use ! on the LHS of equations in Group. Is it possible to expand the specification of Monoid to Group using Haskell type classes? Pat data M = M deriving Show -- Monoid with one operation (!) and identity e (no associativity) class Monoid a where (!) :: a - a - a e :: a a ! e = a -- A Group is a Monoid with an inverse, every Group is a Monoid -- (a necessary condition in logic: Group implies Monoid) -- The inverse property could be expressed as: -- 1) forAll a thereExists b such that a ! b = e -- 2) (inv a) ! a = e class Monoid a = Group a where inverse :: a - a -- Haskell does not like ! on the LHS of equation for inverse in Group. -- (inverse a) ! a = e 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Deciding equality of functions.
On 10/04/2011 04:22, wren ng thornton wrote: The thing is that a lot of the common optimizations (e.g., TCO) completely wreck the inductive structure of the function which, in turn, makes it difficult to say interesting things about them.[1] Could you point me to some Haskell references concerning this point. Thanks, 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Haskell programs as specifications
Hi, Attached are two programs that represent one-way and two-way traffic on a road. I can get the programs to produce reasonable results that match our intuitive ideas of roads. However, I have 2 question about the programs: 1)I cannot get the result suggested by the author that t1 should give true in prog1 and false in prog2. 2)My second question is more theoretical. It is stated by the author that type checking and excitability provide verification. In this case verification probably means checking that an instance is consistent with its type class. Does verification using these techniques in Haskell have any firmer logical foundation than say doing the verification in Java? I am aware that Haskell uses inference for type checking, but is the net result superior to compilers that do not use inference? Also, is Haskell execution based purely on logic? 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-- Ontologies of One-way Roads by Sumit Sen -- http://ifgi.uni-muenster.de/~sumitsen/sen_Font05.pdf -- Two way roads class Link link object | link - object where from, to::link - object other::Eq object = link - object - object other link object | object == from link = to link | object == to link = from link | otherwise = error not linked class Path path object where move :: path - object - object class Named object name | object - name where name :: object - name class LocatedAt object link where location :: object - link --Node type Name = String data Node = Node Name deriving (Eq, Show) -- Edge: A sequence of line segments with nodes at each end data Edge = Edge Node Node deriving Show -- Car data Car = Car Node deriving (Eq, Show) type Cars = [Car] -- a Node is a named object instance Named Node Name where name (Node n) = n -- an Edge as Link between Nodes instance Link Edge Node where from (Edge node1 node2) = node1 to (Edge node1 node2) = node2 -- a Car located at a Node instance LocatedAt Car Node where location (Car node) = node -- Road Element data RoadElement = RoadElement Edge deriving Show class (Path path conveyance ) = Conveyance conveyance path object where transport :: path - conveyance - object - object -- RoadElements as Links between Nodes instance Link RoadElement Node where from (RoadElement edge) = from edge to (RoadElement edge) = to edge -- RoadElements as Paths for Cars instance Path RoadElement Car where move (RoadElement edge) (Car node) = Car (other edge node) -- Algebraic specifications usually depend on (automatic) theorem provers for verification of specifications. -- For our case however type checking and executablity form the basis of verification of our specifications in Haskell. -- This is done by executing test scripts such as -- As orignal paper start = Node start end = Node end theEdge = Edge start end theCar = Car start theRoadElement = RoadElement theEdge t1 = location (move theRoadElement theCar) == end -- Some additional tests -- If start end switched then no linked error theEdge2 = Edge start end theEdge3 = Edgeend start theCar2 = Car start theCar3 = Car end theRoadElement2 = RoadElement theEdge2 theRoadElement3 = RoadElement theEdge3 t2 = location (move theRoadElement2 theCar2) == end t3 = location (move theRoadElement3 theCar3) == start -- In prog2 -- other (Edge (Node start) (Node end)) (Node end) -- gives start -- other (Edge (Node start) (Node end)) (Node start) -- gives end -- Which is what we would expect for a two way street. -- I can get t1, t2 and t3 to give expected results, but I *cannot* get the following to work -- Thus t1 will be true if spec 1 is used and false if spec2 is used deciding if the road specification is of a one way road. -- Ontologies of One-way Roads by Sumit Sen -- http://ifgi.uni-muenster.de/~sumitsen/sen_Font05.pdf --One-way road class Link link object | link - object where from, to::link - object other::Eq object = link - object - object other link object | object == from link = to link | otherwise = error not linked class Path path object where move :: path - object - object class Named object name | object - name where name :: object - name class LocatedAt object link where location :: object - link --Node type Name = String data Node = Node Name deriving (Eq, Show) -- Edge: A sequence of line segments with nodes at each end data Edge = Edge Node Node deriving Show -- Car data Car = Car Node deriving (Eq, Show) type Cars = [Car] -- a Node is a named object instance Named Node Name where name (Node n) = n -- an Edge as Link between Nodes instance Link Edge Node where from (Edge node1 node2) = node1 to (Edge node1 node2) = node2 -- a Car located at a Node instance LocatedAt Car Node where location (Car node) =
Re: [Haskell-cafe] Haskell programs as specifications
Daniel, I think that the definition of other in Link makes bi-directional travel possible in prog1. The function other takes an edge and the first node and returns the other (second) node of that edge. So we can begin our journey at the end and arrive at the start other (Edge (Node end) (Node start)) (Node end) =gives= Node start Or we can begin at the start and end at the end. other (Edge (Node start) (Node end)) (Node start) =gives= Node end So prog1 allows a car to go in both directions. Pat On 03/04/2011 15:39, Daniel Fischer wrote: On Sunday 03 April 2011 16:04:22, Patrick Browne wrote: Hi, Attached are two programs that represent one-way and two-way traffic on a road. I can get the programs to produce reasonable results that match our intuitive ideas of roads. However, I have 2 question about the programs: 1)I cannot get the result suggested by the author that t1 should give true in prog1 and false in prog2. Only took a short look, but that'd probably be because it's wrong, t1 should give True for both. You have a road r from a to b and a car c at a. Then after you move the car along the road, it will be located at b, regardless of whether it's a one- way road or traffic may flow in both directions. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] semantics
Consider the following definitions: 1. Denotational semantics can be considered as relation between syntax and mathematical objects (the meaning of the syntax). 2. Operational semantics can be considered as set of rules for performing computation. Question 1 Applying these definitions in a Haskell context can I say that the lambda calculus provides both the operational and denotational semantics for Haskell programs at value level for definition and evaluations. Question 2 Does it make sense to use these definitions at type level? If so, what exactly do they represent? Thanks, 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] problem with instance method
Hi, I am studying type classes using examples from the literature [1]. The attached code is a formalization of basic object oriented ideas. The particular approach seems to be built on the concepts of: thing, object, and identifier. I have no intension to implement anything or significantly change the code below. Rather, I am trying to understand the code as it stands. I include a number of test runs which seem OK, but I cannot get the *obj* function to work. obj :: t - i - o t i obj t i = Obj t i Any hints would be appreciated. Thanks, Pat [1] ftp://ftp.geoinfo.tuwien.ac.at/frank/frank97executableAxiomaticSpecification.pdf -- A property of a thing data Color = Blue | Green | Red | White deriving Show -- A thing class Cars c where car :: Color - c getColor :: c - Color putColor :: Color - c - c paint :: Color - c - c paint color car = putColor color car data Car = Car Color deriving Show instance Cars Car where car c = Car c putColor color (Car c) = Car color getColor (Car c) = c -- Identifiers for objects class (Integral i) = IDs i where startId :: i newId :: i - i newId i = succ i sameId, notSameId :: i - i - Bool sameId i j = i == j notSameId i j = not (sameId i j) instance IDs Integer where startId = 1 -- Objects consist of Things, with Identifiers class (IDs i, Show i) = Objects o t i where obj :: t - i - o t i getId :: o t i - i getThing :: o t i - t doThing :: (t - t) - o t i - o t i doThing f o = obj (f (getThing o)) (getId o) same :: o t i - o t i - Bool same i j = sameId (getId i) (getId j) isId :: i - o t i - Bool isId i o = sameId i (getId o) -- A general type of Obj data Object t i = Obj t i deriving Show -- A particular Car Obj, which an instance of Objects class (in Haskell terms, not OO terms) instance Objects Object Car Integer where obj t i = Obj t i getId (Obj t i) = i getThing (Obj t i) = t -- Create some actual Objects x = (Obj (Car Blue) (startId::Integer)) y = (Obj (Car Green) (newId startId::Integer)) -- Some tests on car thing, seem OK -- getColor (Car Blue) -- putColor Green (Car Blue) -- getColor (putColor Green (Car Blue)) -- Some tests on objects, seem OK -- same x y -- Obj (Car Blue) (newId startId::Integer) -- Obj (Car Blue) (startId::Integer) -- getThing (Obj (Car Blue) (startId::Integer)) -- getId (Obj (Car Blue) (startId::Integer)) -- isId 2 (Obj (Car Blue) (startId::Integer)) 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Instantiation problem
On 29/01/2011 20:56, Henning Thielemann wrote: Is there a reason why you use an individual type for every unit? The existing implementations of typed physical units only encode the physical dimension in types and leave the unit factors to the value level. I found this to be the most natural way. I am studying type classes using examples from the literature [1]. There is no particular intension to implement anything. I am confused about the unit function in the code below. My understanding is: The signature of the unit function is defined in the MetricDescription class. Any valid instantce of MetricDescription will respect the functional dependency (FD): The FD | description - unit is exactly the signature of the unit function. My confusions I do not understand the definitions of unit in the instances. I do not know how the constant 1 can be equated with a *type*, Where did 1 come from? I do not know how the constant 1 can be equated with *two distinct* definitions of the function uint and still produce the following correct results Ok, modules loaded: A. *A unit (LengthInMetres 7) Metre *A unit (LengthInCentimetres 7) Centimetre *A [1] http://ifgi.uni-muenster.de/~lutzm/odbase04_schade_et_al.pdf == module A where -- Each member of the Unit class has one operator convertFactorToBaseUnit -- that takes a measurement unit (say metre) and returns a conversion factor for that unit of measurement class Unit unit where convertFactorToBaseUnit :: unit - Double class (Unit unit) = MetricDescription description unit | description - unit where unit :: description - unit valueInUnit :: description - Double valueInBaseUnit :: description - Double valueInBaseUnit d = (convertFactorToBaseUnit(unit d)) * (valueInUnit d) data Dog = Dog deriving Show data Metre = Metre deriving Show data Centimetre = Centimetre deriving Show -- An instance for metres, where the convert factor is 1.0 instance Unit Metre where convertFactorToBaseUnit Metre = 1.0 -- An instance for centimetres, where the convert factor is 0.1 instance Unit Centimetre where convertFactorToBaseUnit Centimetre = 0.1 data LengthInMetres = LengthInMetres Double deriving Show data LengthInCentimetres = LengthInCentimetres Double deriving Show instance MetricDescription LengthInMetres Metre where valueInUnit (LengthInMetres d) = d unit l = Metre instance MetricDescription LengthInCentimetres Centimetre where valueInUnit (LengthInCentimetres d) = d unit l = Centimetre 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Instantiation problem
On 30/01/2011 19:43, Henning Thielemann wrote: I do not see a constant 1 that is equated with a type. This is due to my misunderstanding of Haskell. After your comments my understanding of the unit function is as follows: 1) In the instance below the argument for unit must have type LengthInMetres instance MetricDescription LengthInMetres Metre where valueInUnit (LengthInMetres d) = d unit l = Metre 2) The constant 1 on the LHS can be replaced _ because it is the fact that unit is defined in this instance the determines the return value. 3) The RHS is not a type but a constructor. 4) The compiler ensures the correct unit function is called for either MetricDescription instances. Thanks for your help, 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] class-instance
Ryan, This is exactly what I was looking for. Thanks, Pat On 20/01/2011 18:56, Ryan Ingram wrote: On Wed, Jan 19, 2011 at 11:56 PM, Patrick Browne patrick.bro...@dit.ie wrote: I am trying to see what how this requirement can be represented using just the normal instance-implements-class relation for a comparison with a specification language approach. If there is no simple way to do this using type classes then I am obviously mis-using the technique. Going back to your original message: -- My intension is that the PERSON class should *specify* -- that a person has a constant id called p1 -- and that a person has a name that can be found from the id. You can do this with type level numerals. data Z data S a type Zero = Z type One = S Zero type Two = S One -- etc class PersonId a where name :: a - String instance PersonId Z where name _ = John instance PersonId (S Z) where name _ = Julie main = putStrLn (name (undefined :: One)) -- prints Julie -- ryan 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] class-instance
On 19/01/2011 10:41, Ryan Ingram wrote: It's still not really clear what you are trying to do. I am trying to see what how this requirement can be represented using just the normal instance-implements-class relation for a comparison with a specification language approach. If there is no simple way to do this using type classes then I am obviously mis-using the technique. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] class-instance
-- My intension is that the PERSON class should *specify* -- that a person has a constant id called p1 -- and that a person has a name that can be found from the id. class PERSON a b where p1 :: a name :: a - b -- My intension is that the instance should implement the PERSON class instance PERSON Int String where p1 = 1 name p1 = john -- -- Why does the evaluations of p1 or name p1 produce errors? -- how do I fix them and still keep the basic instance-implements-class relation? -- Thanks, -- 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] class-instance
Henning, The code is not intended to fit into a larger application. I am trying to understand instance-implements-class relation. My experiment consists of writing simple English sentences and then seeing how they could be specified and implemented in Haskell. I am sure that this simple requirement could easily be coded in Haskell, but I studying how to specify the requirement using type classes. The bottom line is I want to stay with plain vanilla type classes. If there is no simple way to do this using type classes then I am obviously using the wrong technique. Thanks, Pat On 17/01/2011 11:39, Henning Thielemann wrote: But I suspect, what you try to do is not what you need. If you tell us what you want to do, we can certainly give more helpful answers. Maybe you want to do something with functional dependencies, such that 'String' result type is automatically chosen if the argument type is 'Int'. But before suggesting this type extension, I'd like to know more about your problem. I am trying to understand instance-implements-class relation. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] class-instance
On 17/01/2011 13:04, Ketil Malde wrote: So other PERSONs would have different types, say: I think the problem is there is just one constant p1 in the class and there needs to be multiple constants in the implementation (one for each person). It seems difficult to specify this using type classes So, some data declaration as you suggest will probably be needed. Thanks, 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] class-instance
A functional dependency seems to allow me to express my rather strange requirement. class Person i n | i - n where pid :: i name :: i - n instance Person Int String where pid = 1 name(1) = john -- name(pid::Int) will produce john Thanks for your help Pat On 17/01/2011 14:07, Patrick Browne wrote: On 17/01/2011 13:04, Ketil Malde wrote: So other PERSONs would have different types, say: I think the problem is there is just one constant p1 in the class and there needs to be multiple constants in the implementation (one for each person). It seems difficult to specify this using type classes So, some data declaration as you suggest will probably be needed. Thanks, 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof in Haskell
On 22/12/2010 14:48, Artyom Shalkhakov wrote: ..Do you want to prove a property of a function formally, using some kind of formal logic? I am aware that functional languages do not do proofs at term level, but the motivation for my question is to get a precise reason why this is so. The replies from the café have clearly articulated the reasons. Thanks to all, 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Proof in Haskell
Hi, In a previous posting[1] I asked was there a way to achieve a proof of mirror (mirror x) = x in Haskell itself. The code for the tree/mirror is below: module BTree where data Tree a = Tip | Node (Tree a) a (Tree a) mirror :: Tree a - Tree a mirror (Node x y z) = Node (mirror z) y (mirror x) mirror Tip = Tip The reply from Eugene Kirpichov was: It is not possible at the value level, because Haskell does not support dependent types and thus cannot express the type of the proposition forall a . forall x:Tree a, mirror (mirror x) = x, and therefore a proof term also cannot be constructed. Could anyone explain what *dependent types* mean in this context? What is the exact meaning of forall a and forall x? Thanks, Pat [1] http://www.mail-archive.com/haskell-cafe@haskell.org/msg64842.html 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] commutativity
On 31/10/2010 16:55, Brent Yorgey wrote: Note that the first parameter to commutative shadows the previous definition of com, I don't know if that's what you intended. Does the following avoid the shadowing? infixl 5 `op` op :: Int - Int - Int x `op` y = (x + y) commutative op1 = \a b - (a `op` b) == (b `op` a) 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] commutativity
Hi, Below are two questions on commutative operations in Haskell. infixl 5 `com` com :: Int - Int - Int x `com` y = (x + y) commutative com a b = (a `com` b) == (b`com`a) -- 1 + 3 == 3 + 1 -- This gives true by virtue of the value of LHS and RHS being equal after the plus operation -- Question 1 -- commutative com 1 3 -- This also gives true. Is it because of commutative equation or because of the plus operation? -- Question 2 -- In Haskell can commutativity be specified as a property of infix operations? 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] type level program
Hi, I hypothesize that at type level Haskell offers a form of equational logic. At type level the following program[1] could be interpreted as a first order program in equational logic where; 1)Data types represent declarations of constructors (both constants and functions) 2)Type synonyms represent equations assigning constructors to variables 3)Each class contains a non-constructor operation signature with dependencies 4) instances contain equations that define the operations (similar the term rewriting systems (TRS) of Maude/CafeOBJ). 5):t acts as a reduction or evaluation at type level Is the a reasonable description of this program? Regards, Pat [1] From Fritz Ruehr http://www.willamette.edu/~fruehr/haskell/evolution.html -- static Peano constructors and numerals data Zero data Succ n type One = Succ Zero type Two = Succ One type Three = Succ Two type Four = Succ Three -- dynamic representatives for static Peanos zero = undefined :: Zero one = undefined :: One two = undefined :: Two three = undefined :: Three four = undefined :: Four -- addition, a la Prolog class Add a b c | a b - c where add :: a - b - c instance Add Zerob b instance Add a b c = Add (Succ a) b (Succ c) -- multiplication, a la Prolog class Mul a b c | a b - c where mul :: a - b - c instance Mul Zerob Zero instance (Mul a b c, Add b c d) = Mul (Succ a) b d -- factorial, a la Prolog class Fac a b | a - b where fac :: a - b instanceFac ZeroOne instance (Fac n k, Mul (Succ n) k m) = Fac (Succ n) m -- try, for instance (sorry): -- -- :t fac four 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] running and understanding a lifting program
Patrick,
Thanks for taking the time to get the program running.
It seems fine, but I cannot get the *md* to print out, probably missing
the Show class somewhere.
Thanks again,
Pat
Patrick LeBoutillier wrote:
Patrick,
I found this program interesting and decided to spend a bit of time on
it, even though I'm still a newbie.
I did a few things to simplify the code, here are some comments:
1) I chose to rename the arithmetic functions in the Number class
instead of trying to overload the real ones, I'm not that good at
Haskell yet...
2) The program had some errors, namely I think the definition of the
Point type should be:
data Point a = Point a a
to allow for different types of Points.
3) The Points class seemed useless in the end, I simply defined the
dist function at the top level.
4) If you import Control.Monad, it makes functions (and therefore
Changing v) into a Monad (maybe my terminology is off here...) and
allows you to use the general liftM and liftM2 lifting functions
instead of defining your own.
Here's the complete program:
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
data Point a = Point { x ::a, y :: a }
type Time = Float
-- Functor Changing, which adds time parameter t to its input value.
-- For example, Changing Float indicates a changing floating number
-- (i.e. a function of time).
type Changing v = Time - v
-- Lifting functions
lift1 op a = \t - op (a t)
lift2 op a b = \t - op (a t) (b t)
class Number a where
add, sub, mul :: a - a - a
square, squareRoot :: a - a
square a = a `mul` a
instance Number Float where
add = (+)
sub = (-)
mul = (*)
squareRoot = sqrt
instance Number (Changing Float) where
add = lift2 add
sub = lift2 sub
mul = lift2 mul
squareRoot = lift1 squareRoot
-- The distance operation is defined as follow
dist :: Number a = Point a - Point a - a
dist a b = squareRoot $ square((x a) `sub` (x b)) `add` square ((y a)
`sub` (y b))
-- Running the code
-- If p1 and p2 are two 2D static points,
-- their distance d is calculated as follows:
p1, p2 :: Point Float
p1 = Point 3.4 5.5
p2 = Point 4.5 4.5
-- distance between p1 and p2 -- 1.55
d = dist p1 p2
-- For 2D moving points mp1 and mp2, their distance md,
-- which is a function of time, is calculated as follows:
mp1, mp2 :: Point (Changing Float)
mp1 = Point (\t - 4.0 + 0.5 * t) (\t - 4.0 - 0.5 * t)
mp2 = Point (\t - 0.0 + 1.0 * t) (\t - 0.0 - 1.0 * t)
-- distance between mp1 and mp2
md = dist mp1 mp2
-- distance md for time 2 5.83
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Patrick
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] running and understanding a lifting program
hi, I am trying to run and understand a lifting program from [1]. The program lifts points to moving points that vary their position over time. I made some effort to run the progrm but I do not know how to overide the +,-,*,sqr, and sqrt from the Num class. Below is my current attempt. I do not wish to change or imporve the code, rather I wish to understand it as it stands and find out what needs to be added to get the outputs shown below i.e. distance between points p1 and p2 -- 1.55 and the distance between moving points mp1 and mp2 for time 2 5.83. data Point = Point Float Float data Line = Line Point Point data Polygon = Polygon [Point] type Time = Float -- Functor Changing, which adds time parameter t to its input value. -- For example, Changing Float indicates a changing floating number (i.e. a function of time). type Changing v = Time - v -- The abstract lifting functions class Lifts a where lift0 :: a - f a lift1 :: (a - b) - f a - f b lift2 :: (a - b - c) - f a - f b - f c -- Not too sure about this, instance Lifts Changing Float where lift0 a = \t - a lift1 op a = \t - op (a t) lift2 op a b = \t - op (a t) op (b t) class Number a where (+), (-), (*) :: a - a - a sqr, sqrt :: a - a sqr a = a * a -- The class point which support vector plus and minus as well as -- distance operation is defined as follow class Number s = Points p s where x, y :: p s - s x (Point x1 y1) = x1 y (Point x1 y1) = y1 (+), (-) :: p s - p s - p s (+) a b = Point (x a + x b) (y a + y b) (-) a b = Point (x a - x b) (y a - y b) dist :: p s - p s - s dist a b = sqrt(sqr((x a)-(x b))+sqr((y a)-(y b))) -- The lifting the operations for numbers shoukd provide a distance -- function which can be used for both static and moving points: instance Number v = Number (Changing v) where (+) = lift2 (+) (-) = lift2 (-) (*) = lift2 (*) sqrt = lift1 (sqrt) -- Running the code -- If p1 and p2 are two 2D static points, -- their distance d is calculated as follows: p1, p2 :: Point Float p1 = Point 3.4 5.5 p2 = Point 4.5 4.5 -- distance between p1 and p2 -- 1.55 d = dist p1 p2 -- For 2D moving points mp1 and mp2, their distance md, -- which is a function of time, is calculated as follows: mp1, mp2 :: Point (Changing Float) mp1 = Point (\t - 4.0 + 0.5 * t)(\t - 4.0 - 0.5 * t) mp2 = Point (\t - 0.0 + 1.0 * t)(\t - 0.0 - 1.0 * t) -- distance between mp1 and mp2 md = dist mp1 mp2 -- distance md for time 2 5.83 md 2 [1] A Mathematical Tool to Extend 2D Spatial Operations to Higher Dimensions: by Farid Karimipour1,2, Mahmoud R. Delavar1, and Andrew U. Frank2 http://books.google.ie/books?id=JUGpGN_jwf0Cpg=PA153lpg=PA153dq=Karimipour+%22A+Mathematical+Tool+to+Extend+2D+Spatial+Operations+to+Higher+Dimensions%22source=blots=fu-lSkPMr3sig=ztkcRV3Cv6hn9T6iwQCJ9sB75IMhl=enei=QS7ETJHPGoiA5Ab0zZW6Awsa=Xoi=book_resultct=resultresnum=4ved=0CCMQ6AEwAw#v=onepageq=Karimipour%20%22A%20Mathematical%20Tool%20to%20Extend%202D%20Spatial%20Operations%20to%20Higher%20Dimensions%22f=false 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A model theory question
Alexander Solla wrote: Doing similar constructions with type classes is possible. I think you might have to use witness types (or even a nice functorial wrapper around your target value in the original algebra, or both) to do generalizations of type classes. For example: class Uneditable obj where a :: a - obj b :: b - obj class Refactored obj witness where a' :: Maybe (a - obj) b' :: Maybe (a - obj) data EmptyFilter -- I think the name of the extension needed for this is 'EmptyDataDecls' data NoA data NoB instance Uneditable obj = Refactored obj EmptyFilter where a' = Just a; b' = Just b instance Uneditable obj = Refactored obj NoA where a' = Nothing; b' = Just b Alexander, Thank you for your excellent explanation and example. Due to my lack of knowledge, I do not fully understand what is going in the example. I had a look at the types of a and a’. *Main :t a a :: forall a obj. (Uneditable obj) = a - obj *Main :t a' a' :: forall witness a obj. (Refactored obj witness) = Maybe (a - obj) Could you explain the example a little more. Apologies for my slowness. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A model theory question
Alexander Solla wrote: On 09/26/2010 01:32 PM, Patrick Browne wrote: Bigger how? Under logical implication and its computational analogue? That is to say, do you want the model to be more SPECIFIC, describing a smaller class of objects more richly (i.e, with more logical implications to be made) or do you want the model to be more GENERAL, and contain the less specific submodels? This is how forcing works. My idea of bigger is based on the import modes and parameterized modules of the Maude/CafeOBJ languages, where smaller theories are used to construct larger theories (and/or objects). In these languages I guess theories (loose specifications or interfaces) correspond to your *logical implication* and objects (or tight specification) correspond to *computation* at the ordinary programming level. The axioms of the theories must hold at the programming level. What does the term *forcing* mean? See: http://books.google.ie/books?id=Q0H-n4Wz2ssCpg=PA41lpg=PA41dq=model+expansion+cafeobjsource=blots=_vCFynLmcasig=07V6machOANGM0FTgPF5pcKRrrEhl=enei=YkSgTPn0OoqOjAfb0tWVDQsa=Xoi=book_resultct=resultresnum=1ved=0CBgQ6AEwAA#v=onepageq=model%20expansion%20cafeobjf=false Thanks, 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] A model theory question
Hi, Below is an assumption (which could be wrong) and two questions. ASSUMPTION 1 Only smaller models can be specified using the sub-class mechanism. For example if we directly make a subclass A = B then every instance of B must also be an instance of A (B implies A or B is a subset of A). Hence, type classes cannot be combined using sub-classing to provide specifications of bigger models. QUESTIONS 1) If assumption 1 is correct, is there a mechanism whereby the module system can be used to construct bigger models? 2) If there is such a mechanism does it involve type classes or is it a module only solution? 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] open and closed
Hi,
The details of the issues involved in an open and closed facility for
Haskell are way beyond my current understanding of the language.
Nonetheless, I was wondering does this have anything to do with the
expression problem?
Pat
17/08/2010 14:48 Victor Nazarov asviraspossi...@gmail.com wrote:
Finally tagless technique seems to solve expression problem using
pretty basic Haskell:
--
module AddExp where
class AddExp e
where add :: e - e - e
lit :: Int - e
-- Type signature is required
-- monomorphism restriction will act otherwise
test :: AddExp e = e
test = add (lit 6) (lit 2)
-
module MulExp where
class MulExp e
where mul :: e - e - e
-- Type signature is required
-- monomorphism restriction will act otherwise
test1 :: (AddExp e, MulExp e) = e
test1 = mul test (lit 3)
-
module Evaluator
import AddExp where
newtype Eval = E { eval :: Int }
instance AddExp Eval
where lit = E
add (E a) (E b) = E (a + b)
-
module PrettyPrinter where
import AddExp
import MulExp
newtype PrettyPrint = P { prettyPrint :: String }
instance AddExp (PrettyPrint)
where lit n = show n
add (P a) (P b) = concat [a, + , b]
instance MulExp (PrettyPrint)
where mul (P a) (P b) = concat [a, * , b]
-- Victor Nazarov
Gábor Lehel wrote:
This is pure speculation, inspired in part by Brent Yorgey's blog
post[1] from a few weeks ago.
I'm wondering if it might be possible, in theory, to have both open
and closed variants for each of value-level functions, type functions,
and classes, in a fairly analogous way. (Maybe you could even have
open (G)ADTs, which you would then need open functions to match on; or
maybe a closed one with a case for _ to ensure exhaustiveness.)
In each case you'd have the closed variant requiring you to keep all
the definitions in the same module, permitting overlap, and trying to
match definitions in the order they're listed; whereas the open
variant would let you have definitions across modules, would forbid
overlap (or would require definitions to be equivalent where they
overlap, as with type families), and would always select the uniquely
matching definition.
Open value-level functions with this scheme would be inherently
partial, which is bad. (It's not a problem at the type level because
you just get a compile error if nothing matches, but an exception at
runtime isn't so nice.) As a solution, perhaps it might be possible to
allow a limited form of overlap (or don't even call it overlap) for
the open variants: a default use this is if nothing else matches
definition (which would need to be in the same module as the original
class / type family declaration, or whatever ends up being analogous
for open value-level functions, maybe the type signature). That way
you could use Maybe for open value-level functions and make the
default Nothing, among other options. Overlap in type functions
allegedly makes typechecking unsound; I don't know if that would also
hold in this more limited case. This would definitely break the
property where adding or removing an import can't change the behaviour
of a program other than whether it compiles, which is considered very
important by many [2], so maybe it's not a good solution. (Possibly
you could add explicit import/export control for
instances/other-open-things to alleviate this, in a way so that
definitions for open thingies with default definitions (at least)
would always have to imported explicitly, thereby acknowledging that
it might change behaviour... or maybe that would be a bandaid too far,
I dunno.)
(I think this would also cover most (if not all?) of the use cases for
OverlappingInstances, which permits overlap and selects the most
specific instance in a more general fashion; but maybe that doesn't
matter if the two are equally bad, I don't know. I'm not 100% clear on
peoples' opinion of OverlappingInstances, but I as far as I know the
problems are twofold: both import-unsafeness, and the matter of how
you would actually define most specific in a way that's both
rigorous and intuitive; this would remove at least the latter.)
Anyway, thoughts? Is this all completely crazy and way out there?
[1]
http://byorgey.wordpress.com/2010/08/05/typed-type-level-programming-in-haskell-part-iv-collapsing-types-and-kinds/
[2] http://hackage.haskell.org/trac/haskell-prime/wiki/LanguageQualities
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type classes and logic
Daniel Fischer wrote: class BEING human = HUMAN human where Sub-classing is logical implication BEING(human) = HUMAN(human) All types t that make BEING(t) = true also make HUMAN(t)=true No, it's the other way round. Every HUMAN is also a BEING, hence HUMAN(t) = BEING(t) Could I say that HUMAN is a subset of BEING? Sebastian Fischer wrote: You can define subclasses even if no instances exist. And as Daniel said, the code class BEING human = HUMAN human where defines a subclass HUMAN of BEING which means that every instance of HUMAN must also be a BEING. You can read it as: a BEING is also a HUMAN by the following definitions. Thanks for pointing out my error But I am still not sure of the interpretation of logical implication wrt to sub-classes. Lets simplify the representation and just regard the classes in the example as propositions (instead of predicates). I am not sure if this simplification still makes the example valid. Below is a reasonable interpretation of propositional logical implication. a) If I wear a raincoat then I stay dry (sufficient condition) wareRaincoat = stayDry b) I will stay dry only if I ware a raincoat(necessary condition) stayDry = wareRaincoat In the light of the above examples how should I interpret the class-to-subclass relation as logical implication? Is it a) If BEING then HUMAN (sufficient condition): BEING = HUMAN b) HUMAN is true only if BEING (necessary condition): HUMAN = BEING c) Neither? Thanks, 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] type classes and logic
Hi, I am trying to understand type classes and sub-classes in purely logical terms From the literature I gather that: 1)a type class is a predicate over types (using type variables) 2)type sub-classing is a logical implication between these predicates. But I feel that 1) and 2) does not give enough detail and I am missing the logical significance of the function definitions in the class and their implementations in the instances. This following example outlines my current (mis?)understanding: data Person = Person Name deriving Show data Employee = Employee Name Position deriving Show class BEING being where The class BEING is logically a predicate with type variable being(i.e. BEING(being)) BEING(being) is true for types that are members of the BEING type class. Any types that instantiate the type class BEING will have all the BEING class functions defined on them. Such a type is a member of the type-class BEING Actual function signatures and/or default implementations omitted A proof for the predicate BEING(being) must show that there is an inhabited type (a type which has values) If we find a value for a type that is a proof that a type exists (it is inhabited) that is a member of the class instance BEING Person where All the functions from the class BEING must be defined for the type Person It is required the functions in the instance respect the types from the class and type from the instantiated parameter. t is required that when the functions are run they produce values of the required type. Implementations omitted With at least one instantiation existing (e.g. BEING(Person) = true) we can define a sub-class In the sub-class definition we can assume BEING(human) to be true (type variable name does not matter) And based on that assumption we can write a logical implication BEING(human) = HUMAN(human) class BEING human = HUMAN human where At this point there is no additional functionality is defined for the subclass HUMAN Sub-classing is logical implication BEING(human) = HUMAN(human) All types t that make BEING(t) = true also make HUMAN(t)=true In general for the HUMAN sub-class to be useful additional constraints are added after the where keyword. These are similar in purpose to those described in an ordinary class (not a sub-class) Another example from Bird[1.Intro. to Functional Prog. using Haskell] class Enum a where toEnum :: a - Int fromEnum :: Int - a A type is declared an instance of the class Enum by giving definitions toEnum and fromEnum, functions that convert between elements of the type a and the type Int. In instance declarations fromEnum should be a left inverse to toEnum That is for all x fromEnum(toEnum x) = x. This requirement cannot be expressed in Haskell My questions are: a) Is the above *logical view* of type classes correct? b) What is the logical role of the functions in the classes and instances. Are they constraints on the types in predicates? c) Apart from signature matching between class-to-instance is there any logical relation between the functions in a class and the functions in an instances. From Birds[1] example I suspect that while the types are subject to logical rules of 1) and 2) the actual functions in the instance do not have to obey any logical laws. Any instantiation that respects types is fine? 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type classes and logic
Sebastian, Thanks for your very useful reply. Does the EQ example below not talk about inhabited types as proofs. Thanks, Pat Sebastian Fischer wrote: If we find a value for a type that is a proof that a type exists (it is inhabited) that is a member of the class I don't understand the above statement. The inhabitedness of a type does not tell us anything about which classes it belongs to. Instance declarations do. The EQ example following is from: http://www.haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence A type class in Haskell is a proposition about a type. class Eq a where (==) :: a - a - Bool (/=) :: a - a - Bool means, logically, there is a type a for which the type a - a - Bool is inhabited, or, from a it can be proved that a - a - Bool (the class promises two different proofs for this, having names == and /=). This proposition is of existential nature. A proof for this proposition (that there is a type that conforms to the specification) is (obviously) a set of proofs of the advertised proposition (an implementation), by an instance declaration: instance Eq Bool where True == True = True False == False = True _ == _ = False (/=) a b = not (a == b) 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] expression problem
Hi, The expression problem [1] can be described as the ability to add new variants (either constructors or methods) to a data type without changing the existing code. The Haskell and OO language issues are well described at [1] It seems that the expression problem does not exist in Maude[2]. My question is: Using basic and easy parts of the Haskell, does Haskell currently handle the expression problem. In other words I would like to avoid demanding and sophisticated coding techniques or non-standard Haskell extensions (i.e. it should be easy for the average programmer to use). If there is a simple solution could you please point me to an example. Thanks, Pat [1] Dr. Ralf Laemmel http://channel9.msdn.com/shows/Going+Deep/C9-Lectures-Dr-Ralf-Laemmel-Advanced-Functional-Programming-The-Expression-Problem/ [2]http://lists.cs.uiuc.edu/pipermail/maude-help/2010-January/000336.html 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] data type declaration
Andrew, Thanks for your detailed feedback, it is a great help. I appreciate that the code does not do anything useful, nor is it an appropriate way to write Haskell, but it does help me understand language constructs. I have seen statements like data C3 c3 a = Address c3 a = Address c3 a and wondered what they mean and how could they be used. I am studying the Haskell type class system as part of a language comparison. I am trying to exercise and understand the constructs rather than develop a meaningful application. Perhaps I should have mentioned this in my post. Thanks again, 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] default function definitions
Hi, I am studying the Haskell type class system as part of a language comparison thesis. At this point I am looking at how default function definitions are handled in classes. Functions are usually defined in instances, not classes. I appreciate that the code below may not be an appropriate way to write Haskell programs, but it does help me understand how defaults work. I am not trying to construct a running program. Any feedback on the questions below and defaults work in general would be appreciated. Pat module A where data Person = Person String Integer deriving Show data Employee = Employee String Integer deriving Show class C1 c1 where age :: c1 - Integer -- add default impl, can this be defined only once at class level? -- Can this function be redefined in a *class* lower down the heirarchy? age(c1) = 1 -- Is it true that instances must exists before we can run function or make subclasses? instance C1 Person where instance C1 Employee where -- Is it true that C2 can inherit age, provided an instance of C1 exists class C1 c2 = C2 c2 where name :: c2 - String name(c2) = C2 instance C2 Person where instance C2 Employee where -- Is it true that C3 cannot override C1 or C2 existing defaults? -- Is it true that this must be done at instance level? -- class Cx c3 = C3 c3 where --age(c3) = 3 -- 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] data type declaration
Hi, I am trying to understand the data type declaration below. What is the relation between class C3 and the data type Address below? Where is such a technique used? Thanks, Pat module A where data Person = Person String Integer deriving Show data Employee = Employee String Integer deriving Show class C1 c1 where age :: c1 - Integer instance C1 Person where age(Person P1 1) = 1 instance C1 Employee where age(Employee E1 1) = 1 class C1 c2 = C2 c2 where name :: c2 - String instance C2 Person where name(Person P2 1) = P2 instance C2 Employee where name(Employee E2 1) = E2 class C2 c3 = C3 c3 a where address :: c3 - a instance C3 Person String where -- ** What are the semantics or purpose of this construct. -- ** Is the type declared in the context of a class. data C3 c3 a = Address c3 a = Address c3 a instance C3 Person (Address String String) where 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lambda calculus and equational logic
Patrick Browne wrote: Hi, In Haskell what roles are played by 1)lambda calculus and 2) equational logic? Are these roles related? I think this thread is getting a bit too theoretical, so I moved it to http://lambda-the-ultimate.org/node/4014 Thanks for putting the time and effort into your really helpful replies. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: lambda calculus and equational logic
Heinrich Apfelmus wrote: Lambda calculus is the basis for all three types of semantics: 1) Call-by-need (usually, implementations of Haskell are free to choose other evaluation strategies as long as the denotational semantics match) 2) The denotational semantics of a lambda calculus with general recursion, see also http://en.wikibooks.org/wiki/Haskell/Denotational_semantics 3) Not sure what you mean by proof theoretic semantics. Apparently, the trace of any program execution like, say product [1..5] - 1 * product [2..5] - .. - 120 is a proof that the initial and the final expression denote the same value. The Curry-Howards correspondence is about the type system, viewing types as logical propositions and programs as their proofs. This seems to address the first point (the role of lambda calculus. But what of the second point, the role equational logic. I assume (perhaps incorrectly) that lambda calculus is not *a logic*. See: http://lambda-the-ultimate.org/node/3719 Best 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] lambda calculus and equational logic
In Haskell what roles are played by 1)lambda calculus and 2) equational logic? Are these roles related? Hi, Thanks for your clear and helpful responses. I am aware that this question can lead to into very deep water. I am comparing Haskell with languages based on equational logic (EL) (e.g. Maude/CafeOBJ, lets call them ELLs). I need to identify the fundamental distinction between the semantics of ELLs and Haskell. The focus of my original question was just the purely functional, side effect free, part of Haskell. Semantics can be understood under three headings: *Denotational Semantics; is a model theoretical approach which describes a program in terms of precise mathematical objects (e.g. sets and functions) which provide meaning to a program text. *Operational semantics: provides a technique for computing a result, ELs use term rewriting systems for their operational semantics. *Proof theoretic semantic: syntactically derivable proofs, can use the rules of a logic The relationship between the denotational and the proof theoretic semantic is important for soundness and completeness. Which was sort of behind my original question. Would it be fair to say 1)Lambda calculus provides the operational semantics for Haskell 2)Maybe equational logic provides the denotational semantics. 3)I am not sure of proof theoretic semantic for Haskell. The Curry-Howard correspondence is a proof theoretic view but only at type level. Obviously, the last three points are represent my efforts to address this question. Hopefully the café can comment on the accuracy of these points. Thanks, 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] lambda calculus and equational logic
Hi, In Haskell what roles are played by 1)lambda calculus and 2) equational logic? Are these roles related? Hopefully this question can be answered at a level suitable for this forum. Thanks, 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] understanding Peano
Hi, I would like to understand the Peano module below. I do wish to implement or improve the code. I am unsure of the semantics of (suc = Suc) and then the subsequent use of (Suc n) Is this an example of type-level programming? module Peano where data Nat = Zero | Suc Nat deriving Show class Peano n where suc :: n - n eq :: n - n - Bool plus :: n - n - n instance Peano Nat where suc = Suc eq Zero Zero = True eq (Suc m) (Suc n) = eq m n eq _ _ = False plus m Zero = m plus m (Suc n) = Suc (plus m n) -- Some evaluations let t1 = plus (Suc (Zero)) (Suc ( Suc (Zero))) let t2 = plus (Suc (Suc(Zero))) ( Suc (Zero)) is 1+2=2+1? eq t1 t2 -- true *Peano :t plus (Suc (Suc(Zero))) ( Suc (Zero)) 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] functional dependencies question
Hi,
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 variety
of types (below).
Obviously, some cases are ambigous and/or conflicting and the Haskell
compiler correctly flags this.
Why do some cases such as 1) fail to run even if they are the only
instantiation.
Regards,
Pat
{-
C:\GHC\ghc-6.8.3\bin\ghci.exe -XMultiParamTypeClasses
-XFunctionalDependencies -fglasgow-exts -fallow-undecidable-instances
-}
class LocatedAt object location | object - location where
spatialLocation :: object - location
-- 1) Compiles but does not run
instance LocatedAt Int String where
spatialLocation(1)=home
-- 2) Compiles and runs OK
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
-- 5) Compiles and runs OK, but obviously not in conjunction with 2
instance LocatedAtString Bool where
spatialLocation(home) = True
-- 6) Not OK
instance LocatedAt Float String where
spatialLocation(2.3)=home
-- 7) Compiles but does not run
instance LocatedAt Int Char where
spatialLocation(1)='1'
-- 8) Compiles and runs OK
instance LocatedAt Char Int where
spatialLocation('1')=1
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] functional dependencies question
Neil, Does the following sum up the situation? The class Num has subclasses containing various numeric types and the literal 1 is a value for one or more of those types. Hence the Haskell compiler says the instance 1) is OK. But at run time, without the quantified (1:Int), the 1 could of more than one type, which causes a problem. Thanks for the quick and informative response, Pat Neil Brown wrote: On 01/07/10 12:37, Patrick Browne wrote: Why do some cases such as 1) fail to run even if they are the only instantiation. -- 1) Compiles but does not run instance LocatedAt Int String where spatialLocation(1)=home That instance is fine. I presume the problem is that you are trying to run this function using spatialLocation 1 as the function call. The problem with that is that the 1 part has type Num a = a, i.e. it can be any Num type. Even though you only have one instance, that's not used to constrain the type for 1. The call spatialLocation (1::Int) works correctly. Looking at your other examples, all the ones that don't work have a numeric type for the parameter, so I suspect it is the same issue throughout. Thanks, Neil. 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
