[Flirts] CafeOBJ modules V Haskell type classes

Sun Jun 7 12:45:24 CEST 2009

Hi,
Intorduction
============
I am a PhD student and my thesis is concerned with applying formal
techniques for specifying geographical information systems (GIS).
My background is in GIS and information systems. I do not have that much
expertise in functional languages or formal methods. Nevertheless, my
thesis requires a comparison between Haskell and CafeOBJ (Diaconescu and
Futatsugi 1998; Diaconescu, Futatsugi et al. 2003; Diaconescu 2008).
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).
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.
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)
  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.

For my thesis I wish to compare Haskell and CafeOBJ. Much of this
comparison seems to revolve around 3 points:

1)The higher abstraction and expresive range available in CafeOBJ
equations. For example, a conditional equation for injective property is
executable using the apply command, ceq [inj] : b = b' if g b == g b' .
2) the multiple logics explicitly in CafeOBJ
3) the modularization provided by CafeOBJ modules compared to Haskell's
type classes

Any general comparison between type classes and institution based
languages would probably serve my purpose. In this posting wish to focus
the discussion on point 3 and identify the advantages and dissadvantages
of using institution base module systems over Haskell type classes for
both specifying and prototyping (but not the actual programming of
complex systems). My assumption is that CafeOBJ modules offer better
structuring facilities than Haskell type classes in terms of
encapsulation, a variety of import methods and multiple logics. Not
being a specialist in the area I need some literature or domain expert
to validate this assumption. 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).

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).

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.

3) CMS is based on the logic independent theory of institutions(Goguen
and Burstall 1992).

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?

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).

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).

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. 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.

7) HTC are conceptually predicates on types (Neubauer, Thiemann et al. 2002)

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.

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.

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.
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.
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? Is this a serious drawback for real
specification construction?
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.

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.

Best regards,
Pat Browne
http://www.comp.dit.ie/pbrowne/

References
DeCloss, D. P. (2006). An Analysis Of Specware And Its Usefulness In The
Verification Of High Assurance Systems. Naval Postgraduate School
Monterey, California.

Diaconescu, R. (2005). "Behavioural Specification for Hierarchical
Object Composition." Theoretical Computer Science 343(3): 305-331.

Diaconescu, R. (2008). A Methodological Guide to the CafeOBJ Logic.
Logics of Specification Languages. D. Bjørner and M. Henson, Springer.

Diaconescu, R. and K. Futatsugi (1998). CafeOBJ Report, World Scientific
Publishing Co. Pte. Ltd.

Diaconescu, R., K. Futatsugi, et al. (2003). "CafeOBJ: Logical
Foundations and methodologies." Computing and Informatics 22(Numbers
3-4): 257-283.

Frank, A. and W. Kuhn (1995). Specifying Open GIS with Functional
Languages. In Advances in Spatial Databases (4th International
Symposium, Ssd'95 in Portland, Me), Main, USA., Springer-Verlag, 1995.

Frank, A. U. (1997). Higher order functions necessary for spatial theory
development. Proceedings of Auto-Carto 13, Seattle, USA.

Goguen, J. (1990). Higher-order functions considered unnecessary for
higher-order programming. Research Topics in Functional Programming. D.
Turner, Addison Wesley.

Goguen, J. and R. Burstall (1992). "Institutions: abstract model theory
for specification and programming." Journal of the ACM 39(1): 95-146.

Goguen, J. and K. Lin (2005). Specifying, Programming and Verifying with
Equational Logic. Articles in Honor of Dov Gabbay's 60th Birthday.
Sergei N. Artëmov, Howard Barringer, Artur S. d'Avila Garcez, Luís C.
Lamb and J. Woods, Kings College Press, 2005.

Goguen, J., T. Mossakowski, et al. (2007). "An Institutional View on the
Curry-Howard-Tait-Isomorphism." International Journal of Software
Informatics 1(1): 129–152.

Grenon, P. and B. Smith (2004). "SNAP and SPAN: Towards Dynamic Spatial
Ontology." SPATIAL COGNITION AND COMPUTATION 4(1): 69-104.

Kothar, S. and M. Sulzmann (2005). C++ templates/traits versus Haskell
type classes. Singapore, Technical Report TRB2/05, The National
University of Singapore, 2005.

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.

Meseguer, J. (2003). Executable Computational Logics: Combining Formal
Methods and Programming Langauge Based System Design. MEMOCODE 2003.

Neubauer, M., P. Thiemann, et al. (2002). "Functional logic
overloading." ACM SIGPLAN Notices 37(1): 233-244.

Rabe, F. (2008). Representing Logics and Logic Translations. Computer
Science, Jacobs University Bremen, School of Engineering and Science.
Bremen.

Schroder, L. (2006). Higher Order and Reactive Algebraic Specification
and Development, Department of Computer Science, University of Bremen.

> Basin, D. A. and G. Denker: (2000). \"Maude versus Haskell: an
Experimental Comparison in Security Protocol Analysis.\" Electr. Notes
Theor. Comput. Sci. 36: (2000) 36: (2000).
> 	
> Frank, A., S. Nittel, et al. (2000). Abstract Modeling with Functional
Languages, OPENGIS PROJECT DOCUMENT 00-030.
> 	
> Frank, A. U. and W. Kuhn (1998). A Specification Language for
Interoperable GIS. Interoperating Geographic Information Systems. M. E.
Goodchild, M.J.; Fegeas, R.; Kottman, C., Kluwer Academic Publishers
Norwell, MA, USA.
> 	
> Goguen, J., T. Mossakowski, et al. (2007). \"An Institutional View on
Categorical Logic.\" Int J Software Informatics 1(1): 129-132.
> 	
> Goguen, J., T. Mossakowski, et al. (2007). \"An Institutional View on
the Curry-Howard-Tait-Isomorphism.\" International Journal of Software
Informatics 1(1): 129�152.
> 	
> Kahl, W. and J. Scheffczyk (2001). Named Instances for Haskell Type
Classes. Proc. Haskell Workshop 2001, ENTCS vol. 59 no. 2.
> 	
> Kuhn, W. (2004). Why Information Science needs Cognitive Semantics.
Proceedings of the Workshop on the Potential of Cognitive Semantics for
Ontologies (part of FIOS 2004).
> 	
> Medak, D. (1999). Lifestyles  - A Paradigm for the description of
spatiotemporal  databases. Faculty of Science and Technology. Vienna,
Technical University Vienna. Ph.D.
> 	
> Neubauer, M., P. Thiemann, et al. (2002). \"Functional logic
overloading.\" ACM SIGPLAN Notices 37(1): 233-244.
> 	
> Rabe, F. (2008). Representing Logics and Logic Translations. Computer
Science, Jacobs University Bremen, School of Engineering and Science.
Bremen.
> 	
> Schroder, L. (2006). Higher Order and Reactive Algebraic Specification
and Development, Department of Computer Science, University of Bremen.
> 	
> Schroder, L. (2006). Higher Order and Reactive Algebraic Specification
and Development.
> 	
> Schröder, L. and T. Mossakowski (2002). HasCASL: Towards Integrated
Specification and Development of Haskell Programs. 9th International
Conference on Algebraic Methodology And Software Technology, AMAST 2002,
St. Gilles les Bains, Reunion Island, France, Springer.
> 	
> Schroder, L., T. Mossakowski, et al. (2005). Type class polymorphism
in an institutional framework. Recent Trends in Algebraic Development
Techniques, Springer LNCS. 3423: 234-251.
> 	
> Shields, M. and S. P. Jones (2002). \"First-Class Modules for Haskell.\"
> 	
> Wehr, S. (2005). ML Modules and Haskell Type Classes: A Constructive
Comparison. Institut fur Informatik. Freiburg, Germany., Universitat
Freiburg. MSc.
> 	
>