[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
