[Flirts] Flirts Digest, Vol 5, Issue 2

[pat browne]

Till/Lutz
Thanks for your rapid feedback. Just one comment at the moment.
> I would suggest to use CASL, which is a true first-order language.
> (With the tool Hets, you can even convert ontologies that are
> written in KIF to CASL.)
> But maybe I am missing something.
This would be an obvious choice. I am aware of the work in this area.
But bearing in mind that my target audience are geo-scientists there are
two reasons for not choosing CASL.
1)The perceived one-stop-shop (spec+prog) approach of Haskell is very
appealing. Hence, I feel that I need a single relatively small
environment and CASL may be too big for this work. I feel that CASL
would be very good for specifying at an industrial strength level such
as the OGC (http://www.opengeospatial.org/).
2)Although CASL provides a route to executable code I feel that this is
rather indirect compared to CafeOBJ which provides simple functional and
OO (Lyabakh 2001),( Lechner 1997) languages.

I am working on the BFO ontology which is based on SNAP and SPAN (work
to date attached). The current BFO manual and OWL ontology are at:
http://www.ifomis.org/bfo
Using the syntax of CafeOBJ's OTTER-like prover I have crudely encoded
47 axioms and definitions from an older BFO document (2003) from Grenon
and Smith:
http://ontology.buffalo.edu/smith/articles/SNAP_SPAN.pdf
More work is needed here.

The principle advantage of my approach is that CafeOBJ provides a
complete design and prototyping environment which would be very
difficult to achieve in Haskell. Perhaps my use of CafeOBJ could be
viewed as a first step towards the use of pure specification systems
(like CASL) in the geo-domain.
I will further analyze your response and try to identify definite
situations in which Haskell fails to capture a given geo-semantic that
can be represented by CafeOBJ.

Regards,
Pat
References:
Lechner, U. (1997). Object-oriented specifications of distributed
systems. Dept. of Mathematics and Information, Passau, Germany. 4.
	
Lyabakh, N. (2001). Design and Rigorous Prototyping of Object-Oriented
Modeling with Syntropy., Books on Demand GmbH, Germany.
	





> 
> 
> ------------------------------
> 
> Message: 4
> Date: Mon, 08 Jun 2009 14:47:11 +0200
> From: Till Mossakowski <Till.Mossakowski at dfki.de>
> Subject: Re: [Flirts] CafeOBJ modules V Haskell type classes
> To: "Formalism, Logic, Institution - Relating,	Translating and
> 	Structuring" <flirts at informatik.uni-bremen.de>
> Cc: Lutz Schroeder <Lutz.Schroeder at dfki.de>
> Message-ID: <4A2D084F.9070906 at dfki.de>
> Content-Type: text/plain; charset=UTF-8; format=flowed
> 
> Dear Pat,
> 
> thanks for your interest in Flirts.
> Acutally, you mail is quite long. I hope that this will not hinder
> the discussion too much, since the topic is quite relevant.
> 
>> The Haskell language is very popular among geo-scientist for
>> specification and prototyping (Frank and Kuhn 1995), (Frank 1997). In
>> the geo-domain Haskell has be used in several distinct ways: interface
>> specification language Frank and Kuhn (Frank and Kuhn 1998), an ontology
>> language(Kuhn 2004),  a pure specification language (Frank, Nittel et
>> al. 2000), and a specification and prototyping language (Medak 1999).
> 
> Yes, Werner Kuhn told me about this. I always told him that Haskell
> is not really a specification language, but a programming language.
> You can specify datatypes and profiles of operations in Haskell,
> but not the behaviour of operations.
> 
>> I suspect that institution based languages(Goguen and Burstall 1992),
>> such as CafeOBJ offer a much broader canvas than Haskell in the area of
>> specification and prototyping though not for actual programming.
> 
> Indeed, CafeOBJ is a specification language that also can be used
> for high-level programming.
> 
>> CafeOBJ has a reasonable set logics and proof technologies (equational
>> and a first order OTTER-like theorem prover), model checking (Maude like
>> facilities), and a small object oriented language (FOOPS like). CafeOBJ
>> is also a programming language hence it has some relation with the
>> current practice of using Haskell in the geo-domain. I feel that CafeOBJ
>> has a sufficient set of logics and sufficiently powerful module algebra
>> to allow me to construct a three level geographic model:
>>
>>   Layer 1 consists of an ontology level model that uses First Order
>>   Predicate Logic, based on SNAP and SPAN(Grenon and Smith 2004)
> 
> How do you want to use CafeOBJ for a first-order specification?
> I would suggest to use CASL, which is a true first-order language.
> (With the tool Hets, you can even convert ontologies that are
> written in KIF to CASL.)
> But maybe I am missing something.
> 
>>   Layer 2 consists of domain specific specification of geographic
>>   spatial-temporal objects such as road networks and land parcels.
>>   At this level I use behavioral logic (Diaconescu 2005)and equational
>>   logic (Goguen and Lin 2005).
>>   Layer 3 consists of prototype using Rewriting Logic (Meseguer
>>   2003),(Lechner 1997),(Lyabakh 2001) and equational logic again.
> 
> I guess that layer 3 is about an actual implemented system?
> 
>> Unfortunately, I have found few papers
>> relating these Haskell type classes and modules. Some papers that come
>> close to my required comparison are  (Wehr 2005), (Schr?der and
>> Mossakowski 2002), (Basin and Denker: 2000), (Shields and Jones 2002),
>> (Kahl and Scheffczyk 2001), (Schroder, Mossakowski et al. 2005; Schroder
>> 2006), (Kothar and Sulzmann 2005).
> 
> Actually, I do not know more. Except perhaps the recent development
> that in Isabelle 2009, type classes can be instantiated in
> different ways (using symbol mappings) for one and the same type,
> which comes closer the the CafeOBJ module system than before
> (where they could only be instantiated once per type).
> 
>> My Current understanding
>> =========================
>> Below is my  understanding of the CafeOBJ Module System (CMS) and
>> Haskell Type Classes (HTC).  It may not be possible to focus on the
>> modularity issue in isolation so I have included my understanding of
>> some more general points of comparison between the two languages.
>>
>> 1. Both techniques were originally designed to address different issues,
>> HTC for ad-hoc polymorphism and CMS system structuring. But there seems
>> to be some overlap in there respective usages.  HTC can be used for
>> constructing specifications(Frank 1997) and CMS can be used for a form
>> of higher order programming(Goguen 1990). Note Frank's paper favours
>> higher order functions whereas Goguen's does not. HTC seems to be
>> synonymous with higher order, but some institutions based languages such
>> as Specware are higher order(DeCloss 2006).
> 
> Indeed, you cuold use type classes also in a first-order way, although
> I do not know if this is done.
> The institution approach of course works for higher-order logic as well.
> 
>> 2. HTC is based on Curry-Howard isomorphism between types, propositions
>> and objects of a Cartesian closed category. A HTC is a proposition about
>> a type.
> Yes, but I think that the category needn't be cartesian closed in order
> to define type classes.
> 
>> 3) CMS is based on the logic independent theory of institutions(Goguen
>> and Burstall 1992).
> Agreed.
> 
>> 4) Some work has been done on the unification of Curry-Howard
>> isomorphism and institutions (Goguen, Mossakowski et al. 2007), (Rabe
>> 2008). Is it too naive to say that a foundational level: Institutions
>> are based on model theory and Haskell type classes are based on type theory?
> I would say that roughly describes the situation.
> 
>> 5) Haskell type classes do not provide name spaces (Wehr 2005). Two
>> different type classes cannot define two associated type synonyms or two
>> methods with the same name (unless the two classes are defined in
>> different Haskell modules).
> Agreed.
> 
>> 6) Type classes and instances in Haskell 98 may contain only methods;
>> extensions to Haskell 98 also allow type synonyms (e.g. type Name =
>> String ) and data types (e.g. data Anniversary = Birthday Date | Wedding
>> Date).(Wehr 2005). There exists no extension that allows nested type
>> classes and instances (Wehr 2005).
> Indeed, this and the previous point show the advantages of CMS.
>> 5) My interpretation is that a loose module in CafeOBJ roughly
>> corresponds to a Haskell class, while a tight module corresponds to a
>> Haskell instance.
> OK, but this is a very rough correspondence.
> I would put it this way: you can simulate type classes with certain
> loose modules and instances with certain tight modules.
> 
>   CafeOBJ modules can be parameterized by other modules
>> whereas Haskell class/instances are parameterized by types. CafeOBJ
>> modules can also import other modules. This importation includes
>> facilities to rename elements (sorts and functions). Importation also
>> allows the user to construct logically valid mappings between elements
>> in the imported module and the importing module. Haskell type classes do
>> not import in this sense, their only structuring mechanisms are
>> parameterization (by classes or type?) and inheritance of other classes.
>> True importing in Haskell is handled by Haskell's own module system
>> which operates above and independently of the type class system. The
>> Haskell module can handle HTC.
>>
>> 6) The instances of HTC are not named in standard Haskell whereas all
>> CafeOBJ modules and views are named.
> Yes, and Isabelle 2009 goes beyond that (see above).
> 
>> 7) HTC are conceptually predicates on types (Neubauer, Thiemann et al. 2002)
> Agreed.
> 
>> 8) Frank and Kuhn (Frank and Kuhn 1998) assert that classes in Haskell
>> describe (define?) classes of algebras and instances define particular
>> models. This seems to be pretty close to what modules can achieve.
> see my remark to 5)
> 
>> 9) In Haskell class instances may be spread over several
>> modules(Neubauer, Thiemann et al. 2002). Issues: Order of imports (no
>> colimit). Where is the class declared? Are their conflicting instances?.
>> 10) While it is possible to reason about a Haskell program the logic of
>> Haskell is not always explicitly present. Some formal reasoning can be
>> done but no formal semantic is written for Haskell. This makes it
>> difficult to write formal tools for Haskell. This point may be more
>> related to what is in a module than how modules may be combined.
> 
> You are right that there is no complete formal semantics for Haskell.
> Still, there are some translations of Haskell (subsets) to theorem
> provers that allow reasoning about Haskell (Isabelle-Haskabelle, Hets,
> Programatica).
>> Question.
>> ========
>> I now have a set of questions that should help me identify the relative
>> strengths and weakness of HTC and CMS:
>> Question 1:
>> Is my rough understand of HTC and CMS reasonable? Obviously, I am not
>> talking at a very detailed or formal level, but from the point of view
>> of a user who wishes to construct specifications and understand the
>> basics of strengts and limitations of each approach.
> Yes, see my comments above.
> 
>> Question 2:
>> Notwithstanding my current understanding of Haskell set out above, is
>> there any way of 'importing'(in the CafeOBJ sense) type classes into
>> type classes or instances into instances.
> I don't think so. I am not even sure what this should mean.
> 
> A way of combining type classes with module imports similar
> to those of CafeOBJ is provided by HasCASL. But this does not mean that
> you can import type classes with type classes.
> 
>> Question 3:
>> Lutz Schroder (Schroder 2006) talks about type classes being a
>> 'pre-institution' for polymorphism. My understanding of his paper is
>> that type classes do not support 'model expansion', because expanded
>> models may have more types. Is this due to the lack of an import
>> facility in Haskell's type classes? 
> No, this is more a theoretical problem: proving the satisfacition
> condition for institutions featuring ad-hoc-polymorphism is hard,
> because polymorphism speaks about all possible types, which
> may be available only in future expansions of a model.
> 
> Is this a serious drawback for real
>> specification construction?
> I do not think so.
> 
>> Question 4: Haskell type classes can be used to express axioms about
>> their operations (loose model or theoy). We can have many instances of a
>> class(each a tight model). These can be combined in various ways with
>> instances of other classes. But I am not sure if HTC has the ability to
>> mix loose and initial models.
> In a sense, Haskell's type classes provide a very specific form of
> looseness, namely you can think of the interface of the type class
> being a loose specification that must be matched by the instances.
> Everything else is equipped with a ("tight") fixed-point semantics
> (which can be considered as some kind of initial semantics, but
> in a different category of models than for CafeOBJ).
> 
>> Conclusion.
>> ==========
>> I hope that my questions are not to naive or off the mark. What I really
>> need is a set of theoretically sound advantages and disadvantages of CHS
>> and HTC. Intuitively I feel the CMS is superior to HTC for specification
>> but I cannot prove or even intelligently articule this point. These
>> advantages and disadvantage should be understood by average computer
>> practitioner and geo-scientist who has little knowledge of formal
>> methods but is willing to put in an effort to gain enough knowledge to
>> grasp the main issues.
> 
> This sounds like a significant but also quite difficult task.
> 
> With all best wishes,
> Till
> 

-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: SNAPSPAN2.txt
URL: <http://www.informatik.uni-bremen.de/pipermail/flirts/attachments/20090608/2b81e037/attachment-0001.txt>