[Haskell-cafe] Approaches to dependent types (DT)
Hi, I am trying to understand the concept of dependent types as described in Haskell literature (Hallgren 2001),(Hinze,Jeuring et al. 2006). I am particularly interested in understanding two flavours of dependency mentioned by Hinze et al: 1) Types depending on values called dependent types 2) Types depending on types called parametric and type-indexed types I think that ascending levels of abstraction are important here: values - types - classes (Hallgren 2001). Here is a Haskell example of the use of DT: class Named object name | object - name where name :: object - name instance (Eq name, Named object name) = Eq object where object1 == object2 = (name object1) == (name object2) I think that the intended semantics are: 1) Objects have names and can be compared for equality using these names. 2) Two objects are considered equal (identical) if they have the same name. 3) The type of a name depends on the type of the object, which gets expressed as a type dependency (object - name). I am not sure about the last semantic it might be interpreted as the named object depends on... This may indicate a flaw in my understanding of DT. I am aware that dependent types can be used to express constraints on the size of lists and other collections. My understanding of Haskell's functional dependency is that object - name indicates that fixing the type object should fix the type name (equivalently we could say that type name depends on type object). The class definition seems to show a *type-to-type* dependency (object to name), while the instance definition shows how a name value is used to define equality for objects which could be interpreted as a *value-to-type* dependency (name to object) in the opposite direction to that of the class. My questions are: Question 1: Is my understanding correct? Question 2: What flavour of DT is this does this example exhibit? Best regards, Pat Hallgren, T. (2001). Fun with Functional Dependencies. In the Proceedings of the Joint CS/CE Winter Meeting, Varberg, Sweden, January 2001. Hinze, R., J. Jeuring, et al. (2006). Comparing Approaches to Generic Programming in Haskell. Datatype-generic programming: international spring school, SSDGP 2006. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Merging modules
Hi, I want to establish the strengths and weakness of the Haskell module system for the ontology merging task (I know it was not designed for this!). I wish to make a new module (MERGEDONTOLOGY) from three input modules one of which is common to the other two. The desired merge should contain the following data types: Woman FinancialBank HumanBeing RiverBank Which are all identifiable without any qualifying module names. Below is the detailed requirement and my first attempt at this task in Haskell. I would be grateful for any information on how to merge these modules giving a set of unique unqualified types (i.e. without reference to their originating modules). Regards, Pat Informal Specification The diagram and text below explain the requirement MERGEDONTOLOGY { Woman, RiverBank, FinancialBank, HumanBeing} /\ /\ / \ /\ / \ / \ / \ / \ ONTOLOGY1 ONTOLOGY2 {Woman, Bank, Person} {Woman, Bank, Human} /\ /\ \ / \ / \ / \ / \ / \ / \ / {Woman , Person} COMMMON This example includes both synonyms and homonyms. 1)The Woman sort (or data type) should be the same in all modules, there is only one Woman sort and it is named as such in each module. Hence there should be only one MERGEDONTOLOGY.Woman. 2)There is only one sort MERGEDONTOLOGY.HumanBeing, but there are 3 synonyms for it called ONTOLOGY2.Human, ONTOLOGY1.Person, and COMMON.Person. The last sentence considers ONTOLOGY1.Person and COMMON.Person as synonyms; they have different qualifiers but the intention is that they represnt the same thing. Hence should be mapped to same MERGEDONTOLOGY.HumanBeing. To do this (in Maude) COMMON.Person was renamed to ONTOLOGY2.Human which in turn was renamed to MERGEDONTOLOGY.HumanBeing. 3)The homonyms are ONTOLOGY1.Bank and ONTOLOGY2.Bank should become distinct sorts MERGEDONTOLOGY.RiverBank and MERGEDONTOLOGY.FinancialBank in the final ontology at the top of the diagram. My first attemt at merging using Haskell modules = module COMMON where data Woman = WomanC data Person = PersonC module ONTOLOGY1 where import COMMON data Bank = BankC module ONTOLOGY2 where import COMMON data Bank = BankC module MERGEDONTOLOGY where import ONTOLOGY1 import ONTOLOGY2 If I use qualified names all the constructors are interpreted correctly MERGEDONTOLOGY :t COMMON.WomanC COMMON.WomanC :: COMMON.Woman MERGEDONTOLOGY :t COMMON.PersonC COMMON.PersonC :: COMMON.Person MERGEDONTOLOGY :t ONTOLOGY2.BankC ONTOLOGY2.BankC :: ONTOLOGY2.Bank MERGEDONTOLOGY :t ONTOLOGY1.BankC ONTOLOGY1.BankC :: ONTOLOGY1.Bank MERGEDONTOLOGY :t COMMON.Woman However, I wish that these types and constructors be fully defined in the context of the MERGEDONTOLOGY. I have tried type synonyms and newtypes. type RiverBank = ONTOLOGY1.Bank type FinancialBank = ONTOLOGY2.Bank newtype RiverBank = BankC Int I have not explored import modes or qualified imports. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Merging modules
This is all pretty basic stuff. Not sure any of it is very helpful. (Why do you want to spread an ontology over several Haskell modules?) -matthias Yes it is very helpful, I have limited time to study Haskell. The reason for spreading the information over modules is to simulate actual ontologies and the mappings to other ontologies. My next step is, as you suggested, to use type classes. My overall thesis is the study of current algebraic specification and programming techniques. Thanks, Pat mf-hcafe-15c311...@etc-network.de wrote: On Fri, Oct 16, 2009 at 11:42:22AM +0100, pat browne wrote: To: haskell-cafe@haskell.org From: pat browne patrick.bro...@comp.dit.ie Date: Fri, 16 Oct 2009 11:42:22 +0100 Subject: [Haskell-cafe] Merging modules Hi, I want to establish the strengths and weakness of the Haskell module system for the ontology merging task (I know it was not designed for this!). I wish to make a new module (MERGEDONTOLOGY) from three input modules one of which is common to the other two. The desired merge should contain the following data types: Woman FinancialBank HumanBeing RiverBank Which are all identifiable without any qualifying module names. Below is the detailed requirement and my first attempt at this task in Haskell. I would be grateful for any information on how to merge these modules giving a set of unique unqualified types (i.e. without reference to their originating modules). Regards, Pat Informal Specification The diagram and text below explain the requirement MERGEDONTOLOGY { Woman, RiverBank, FinancialBank, HumanBeing} /\ /\ / \ /\ / \ / \ / \ / \ ONTOLOGY1 ONTOLOGY2 {Woman, Bank, Person} {Woman, Bank, Human} /\ /\ \ / \ / \ / \ / \ / \ / \ / {Woman , Person} COMMMON This example includes both synonyms and homonyms. 1)The Woman sort (or data type) should be the same in all modules, there is only one Woman sort and it is named as such in each module. Hence there should be only one MERGEDONTOLOGY.Woman. 2)There is only one sort MERGEDONTOLOGY.HumanBeing, but there are 3 synonyms for it called ONTOLOGY2.Human, ONTOLOGY1.Person, and COMMON.Person. The last sentence considers ONTOLOGY1.Person and COMMON.Person as synonyms; they have different qualifiers but the intention is that they represnt the same thing. Hence should be mapped to same MERGEDONTOLOGY.HumanBeing. To do this (in Maude) COMMON.Person was renamed to ONTOLOGY2.Human which in turn was renamed to MERGEDONTOLOGY.HumanBeing. 3)The homonyms are ONTOLOGY1.Bank and ONTOLOGY2.Bank should become distinct sorts MERGEDONTOLOGY.RiverBank and MERGEDONTOLOGY.FinancialBank in the final ontology at the top of the diagram. My first attemt at merging using Haskell modules = module COMMON where data Woman = WomanC data Person = PersonC module ONTOLOGY1 where import COMMON data Bank = BankC module ONTOLOGY2 where import COMMON data Bank = BankC module MERGEDONTOLOGY where import ONTOLOGY1 import ONTOLOGY2 If I use qualified names all the constructors are interpreted correctly MERGEDONTOLOGY :t COMMON.WomanC COMMON.WomanC :: COMMON.Woman MERGEDONTOLOGY :t COMMON.PersonC COMMON.PersonC :: COMMON.Person MERGEDONTOLOGY :t ONTOLOGY2.BankC ONTOLOGY2.BankC :: ONTOLOGY2.Bank MERGEDONTOLOGY :t ONTOLOGY1.BankC ONTOLOGY1.BankC :: ONTOLOGY1.Bank MERGEDONTOLOGY :t COMMON.Woman However, I wish that these types and constructors be fully defined in the context of the MERGEDONTOLOGY. I have tried type synonyms and newtypes. type RiverBank = ONTOLOGY1.Bank type FinancialBank = ONTOLOGY2.Bank newtype RiverBank = BankC Int I have not explored import modes or qualified imports. The way you import ONTOLOGY* and COMMON without qualified, you can use any name that you import without qualifier
[Haskell-cafe] Merging classes
Hi, Following on from my earlier *Merging modules* email, where I tried to simulate ontology merging with Haskell modules; http://article.gmane.org/gmane.comp.lang.haskell.cafe/64943 I *think* that the type of merging that I am attempting is difficult with modules so I gave classes a try. I did not get very far (see below). Perhaps I need a combination of type classes and modules. In fairness this is more of a specification task than a programming task and perhaps I am barking up the wrong tree. Any help appreciated. Regards, Pat == attempting an ontology merge with type classes For specification of requirement see http://article.gmane.org/gmane.comp.lang.haskell.cafe/64943 == -- Data types for COMMON data Woman = WomanC data Person = PersonC -- Additional data type for ONTOLOGY1 data Bank = BankC -- Additional data type for ONTOLOGY2 -- but how do I let type Bank have the same name in both classes and -- still be distinct (homonyms) in the merged class -- data Bank = BankC class COMMON a b where class (COMMON a b) = ONTOLOGY1 a b where class (COMMON a b) = ONTOLOGY2 a b where class (ONTOLOGY1 a b, ONTOLOGY2 a b) = MERGEDONTOLOGY a b where -- not really sure how to proceed from here instance COMMON Woman Person where ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Approaches to dependent types (DT)
Petr, Thanks for the links. My research involves the study of current algebraic specification and programming languages. I have posted some very general and abstract style questions in order to get a better feel of the individual languages. I do not wish to become highly proficient in each language, so any links that speed up my research are much appreciated. Thanks again, Pat Petr Pudlak wrote: Hi Pat, you might be interested in Agda [1] and the tutorial Dependently Typed Programming in Agda [2]. I'm just reading the tutorial and it helps me a lot with understanding the concept. Also if you'd like to have a deeper understanding of the underlying theory, I'd suggest reading Barendregt's Lambda Calculi with Types [3]. Best regards, Petr [1] http://wiki.portal.chalmers.se/agda/ [2] http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf [3] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.4391 and ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z On Fri, Oct 09, 2009 at 02:11:30PM +0100, pat browne wrote: Hi, I am trying to understand the concept of dependent types as described in Haskell literature (Hallgren 2001),(Hinze,Jeuring et al. 2006). I am particularly interested in understanding two flavours of dependency mentioned by Hinze et al: 1) Types depending on values called dependent types 2) Types depending on types called parametric and type-indexed types I think that ascending levels of abstraction are important here: values - types - classes (Hallgren 2001). Here is a Haskell example of the use of DT: class Named object name | object - name where name :: object - name instance (Eq name, Named object name) = Eq object where object1 == object2 = (name object1) == (name object2) I think that the intended semantics are: 1) Objects have names and can be compared for equality using these names. 2) Two objects are considered equal (identical) if they have the same name. 3) The type of a name depends on the type of the object, which gets expressed as a type dependency (object - name). I am not sure about the last semantic it might be interpreted as the named object depends on... This may indicate a flaw in my understanding of DT. I am aware that dependent types can be used to express constraints on the size of lists and other collections. My understanding of Haskell's functional dependency is that object - name indicates that fixing the type object should fix the type name (equivalently we could say that type name depends on type object). The class definition seems to show a *type-to-type* dependency (object to name), while the instance definition shows how a name value is used to define equality for objects which could be interpreted as a *value-to-type* dependency (name to object) in the opposite direction to that of the class. My questions are: Question 1: Is my understanding correct? Question 2: What flavour of DT is this does this example exhibit? Best regards, Pat Hallgren, T. (2001). Fun with Functional Dependencies. In the Proceedings of the Joint CS/CE Winter Meeting, Varberg, Sweden, January 2001. Hinze, R., J. Jeuring, et al. (2006). Comparing Approaches to Generic Programming in Haskell. Datatype-generic programming: international spring school, SSDGP 2006. ___ 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
[Haskell-cafe] Re: Merging modules (again)
Hi, I have tried qualified imports, synonyms and newtypes but still I could not implement the merging task (previously posted). This is probably because I have little knowledge of Haskell *or* the task is not really suited to Haskell (more of a specification task than a programming task). My main questions are; Can the merging task be achieved using the Haskell module system? I also posted a question on how this task could be done using type classes. I would ask the same question with respect to type classes. Regards, Pat pat browne wrote: Hi, I want to establish the strengths and weakness of the Haskell module system for the ontology merging task (I know it was not designed for this!). I wish to make a new module (MERGEDONTOLOGY) from three input modules one of which is common to the other two. The desired merge should contain the following data types: Woman FinancialBank HumanBeing RiverBank Which are all identifiable without any qualifying module names. Below is the detailed requirement and my first attempt at this task in Haskell. I would be grateful for any information on how to merge these modules giving a set of unique unqualified types (i.e. without reference to their originating modules). Regards, Pat Informal Specification The diagram and text below explain the requirement MERGEDONTOLOGY { Woman, RiverBank, FinancialBank, HumanBeing} /\ /\ / \ /\ / \ / \ / \ / \ ONTOLOGY1 ONTOLOGY2 {Woman, Bank, Person} {Woman, Bank, Human} /\ /\ \ / \ / \ / \ / \ / \ / \ / {Woman , Person} COMMMON This example includes both synonyms and homonyms. 1)The Woman sort (or data type) should be the same in all modules, there is only one Woman sort and it is named as such in each module. Hence there should be only one MERGEDONTOLOGY.Woman. 2)There is only one sort MERGEDONTOLOGY.HumanBeing, but there are 3 synonyms for it called ONTOLOGY2.Human, ONTOLOGY1.Person, and COMMON.Person. The last sentence considers ONTOLOGY1.Person and COMMON.Person as synonyms; they have different qualifiers but the intention is that they represnt the same thing. Hence should be mapped to same MERGEDONTOLOGY.HumanBeing. To do this (in Maude) COMMON.Person was renamed to ONTOLOGY2.Human which in turn was renamed to MERGEDONTOLOGY.HumanBeing. 3)The homonyms are ONTOLOGY1.Bank and ONTOLOGY2.Bank should become distinct sorts MERGEDONTOLOGY.RiverBank and MERGEDONTOLOGY.FinancialBank in the final ontology at the top of the diagram. My first attemt at merging using Haskell modules = module COMMON where data Woman = WomanC data Person = PersonC module ONTOLOGY1 where import COMMON data Bank = BankC module ONTOLOGY2 where import COMMON data Bank = BankC module MERGEDONTOLOGY where import ONTOLOGY1 import ONTOLOGY2 If I use qualified names all the constructors are interpreted correctly MERGEDONTOLOGY :t COMMON.WomanC COMMON.WomanC :: COMMON.Woman MERGEDONTOLOGY :t COMMON.PersonC COMMON.PersonC :: COMMON.Person MERGEDONTOLOGY :t ONTOLOGY2.BankC ONTOLOGY2.BankC :: ONTOLOGY2.Bank MERGEDONTOLOGY :t ONTOLOGY1.BankC ONTOLOGY1.BankC :: ONTOLOGY1.Bank MERGEDONTOLOGY :t COMMON.Woman However, I wish that these types and constructors be fully defined in the context of the MERGEDONTOLOGY. I have tried type synonyms and newtypes. type RiverBank = ONTOLOGY1.Bank type FinancialBank = ONTOLOGY2.Bank newtype RiverBank = BankC Int I have not explored import modes or qualified imports. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] matching types in Haskell
Hi, I wish to align or match some Haskell types in order to represent a set of ontologies and their embedded concpts [1]. I am not sure wheather modules or classes could be used. I have done this task in a language called Maude[2]. The code is below. I appreciate that Maude is not very popular so there is a brief description below. This diagram below represents the semantics of what I am trying to achive. I want to construct MERGEDONTOLOGY from ONTOLOGY1 and ONTOLOGY2 both of which are based on COMMON. MERGEDONTOLOGY { Woman, RiverBank, FinancialBank, HumanBeing} /\ /\ / \ /\ / \ / \ / \ / \ ONTOLOGY1 ONTOLOGY2 {Woman, Bank, Person} {Woman, Bank, Human} /\ /\ \ / \ / \ / \ / \ / \ / \ / {Woman , Person} COMMMON Each Maude module represents (below) a distinct ontology, each sort (or type in Haskell) represents a concept. This example includes both synonyms and homonyms. I want to align ONTOLOGY1 and ONTOLOGY2 w.r.t COMMON to produce MERGEDONTOLOGY. The details of the concepts are as follows. The Woman concept should be the same in all ontologies, there is only one Woman concept and it is named as such in each ontology. Hence there should be only one Woman.MERGEDONTOLOGY There is only one concept HumanBeing.MERGEDONTOLOGY, but there are 3 synonyms Human.ONTOLOGY2, Person.ONTOLOGY1, and Person.COMMON It would seem that Person.COMMON should be mapped (or renamed?) to Human.ONTOLOGY2 which in turn is renamed (or mapped) to HumanBeing.MERGEDONTOLOGY. The homonyms are Bank.ONTOLOGY1 and Bank.ONTOLOGY2 which should become distinct entities in RiverBank.MERGEDONTOLOGY and FinancialBank.MERGEDONTOLOGY My question is how should this be done in Haskell. Is there a classes only solution? Is ther a module only solution? Or do I need both? Regards, Pat = Brief description of Maude code In the Maude Language the module is the basic conceptual unit. Sorts are declared in modules Every line ends with a space dot. In this case each module is bracketed by fth .. endfth There are various types of mappings between modules. In this case I used renamings where the syntax is *( name_in_source_module to name_in_target_module) The keyword protecting is a type of inport. The + symbol between the modules forms a new module that includes all the information in each of its arguments == fth COMMON is sorts Woman Person . endfth fth ONTOLOGY1 is protecting COMMON . sorts Bank . endfth fth ONTOLOGY2 is protecting COMMON *( sort Person to Human) . sorts Bank . endfth fth MERGEDONTOLOGY is including (ONTOLOGY1 * (sort Bank to RiverBank,sort Person to HumanBeing)) + (ONTOLOGY2 * (sort Human to HumanBeing, sort Bank to FinancialBank)) . endfth with the command show all MERGEDONTOLOGY the system will produce the following module fth MERGEDONTOLOGY0 is sorts Woman HumanBeing FinancialBank RiverBank . endfth Reference [1]Shapes of Alignments Construction, Combination, and Computation by Oliver Kutz, Till Mossakowsk, and Mihai Codescu http://www.informatik.uni-bremen.de/~okutz/shapes.pdf [2] Informa tiom on Maude at: http://maude.cs.uiuc.edu/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Peano axioms
Hi, Below are two attempts to define Peano arithmetic in Haskell. The first attempt, Peano1, consists of just a signature in the class with the axioms in the instance. In the second attempt, Peano2, I am trying to move the axioms into the class. The reason is, I want to put as much specification as possible into the class. Then I would like to include properties in the class such as commutativity something like: infixl 5 `com` com :: Int - Int - Int x `com` y = (x + y) commutative com a b = (a `com` b) == (b `com` a) I seem to be able to include just one default equation the Peano2 attempt. Any ideas? I have looked at http://www.haskell.org/haskellwiki/Peano_numbers Regards, Pat -- Attempt 1 -- In this attempt the axioms are in the instance and things seem OK module Peano1 where infixl 6 `eq` infixl 5 `plus` class Peano1 n where suc :: n - n eq :: n - n - Bool plus :: n - n - n data Nat = One | Suc Nat deriving Show instance Peano1 Nat where suc = Suc One `eq` One = True (Suc m) `eq` (Suc n) = m `eq` n _`eq`_ = False m `plus` One = Suc m m `plus` (Suc n) = Suc (m `plus` n) -- Evaluation *Peano1 Suc(One) `plus` ( Suc (One)) -- Attempt 2 -- In this attempt the axioms are in the class and things are not OK. module Peano2 where infixl 6 `eq` infixl 5 `plus` class Peano2 n where one :: n eq :: n - n - Bool plus :: n - n - n suc :: n - n suc a = a `plus` one {- I cannot add the remaining default axioms one `eq` one = True (suc m) `eq` (suc n) = m `eq` n (suc a) `eq` (suc b) = a `eq` b _`eq`_ = False -} ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Proof in Haskell
Hi, Below is a function that returns a mirror of a tree, originally from: http://www.nijoruj.org/~as/2009/04/20/A-little-fun.html where it was used to demonstrate the use of Haskabelle(1) which converts Haskell programs to the Isabelle theorem prover. Isabelle was used to show that the Haskell implementation of mirror is a model for the axiom: mirror (mirror x) = x My question is this: Is there any way to achieve such a proof in Haskell itself? GHC appears to reject equations such has mirror (mirror x) = x mirror (mirror(Node x y z)) = Node x y z Regards, Pat =CODE= 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 (1)Thanks to John Ramsdell for the link to Haskabelle: http://www.cl.cam.ac.uk/research/hvg/Isabelle/haskabelle.html). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] river crossing puzzle
Hi, Does anyone know where there are any Haskell implementations of the the River Crossing puzzle (AKA Farmer/Fox/Goose/Grain). There are several variations but the general ideas are explained at: http://en.wikipedia.org/wiki/River_crossing_puzzle http://en.wikipedia.org/wiki/Fox,_goose_and_bag_of_beans_puzzle I have found one at: http://www.shido.info/hs/haskell9.html Thanks, Pat ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe