From Patrick.Browne at comp.dit.ie Sun Jun 7 12:45:24 2009 From: Patrick.Browne at comp.dit.ie (pat browne) Date: Sun, 07 Jun 2009 11:45:24 +0100 Subject: [Flirts] CafeOBJ modules V Haskell type classes Message-ID: <4A2B9A44.3040409@comp.dit.ie> 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. > > From Till.Mossakowski at dfki.de Mon Jun 8 14:47:11 2009 From: Till.Mossakowski at dfki.de (Till Mossakowski) Date: Mon, 08 Jun 2009 14:47:11 +0200 Subject: [Flirts] CafeOBJ modules V Haskell type classes In-Reply-To: <4A2B9A44.3040409@comp.dit.ie> References: <4A2B9A44.3040409@comp.dit.ie> Message-ID: <4A2D084F.9070906@dfki.de> 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 -- Till Mossakowski Cartesium, room 2.051 Phone +49-421-218-64226 DFKI GmbH Bremen Fax +49-421-218-9864226 Safe & Secure Cognitive Systems Till.Mossakowski at dfki.de Enrique-Schmidt-Str. 5, D-28359 Bremen http://www.dfki.de/sks/till Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH principal office, *not* the address for mail etc.!!!: Trippstadter Str. 122, D-67663 Kaiserslautern management board: Prof. Wolfgang Wahlster (chair), Dr. Walter Olthoff supervisory board: Prof. Hans A. Aukes (chair) Amtsgericht Kaiserslautern, HRB 2313 From Patrick.Browne at comp.dit.ie Mon Jun 8 19:23:37 2009 From: Patrick.Browne at comp.dit.ie (pat browne) Date: Mon, 08 Jun 2009 18:23:37 +0100 Subject: [Flirts] Flirts Digest, Vol 5, Issue 2 In-Reply-To: References: Message-ID: <4A2D4919.30002@comp.dit.ie> 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 > Subject: Re: [Flirts] CafeOBJ modules V Haskell type classes > To: "Formalism, Logic, Institution - Relating, Translating and > Structuring" > Cc: Lutz Schroeder > 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: From Till.Mossakowski at dfki.de Tue Jun 9 16:42:59 2009 From: Till.Mossakowski at dfki.de (Till Mossakowski) Date: Tue, 09 Jun 2009 16:42:59 +0200 Subject: [Flirts] Flirts Digest, Vol 5, Issue 2 In-Reply-To: <4A2D4919.30002@comp.dit.ie> References: <4A2D4919.30002@comp.dit.ie> Message-ID: <4A2E74F3.5000808@dfki.de> Dear Pat, > 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. I know BFO as a first-order ontology. But it seems that CafeOBJ can handle first-order logic by encoding the rules for FOL somehow in membership equational logic? Still, I think the specialised first-order provers that are connected to Hets (for proving in CASL) have better performance, since they are the best at the annual CASC competition. All the best, Till -- Till Mossakowski Cartesium, room 2.051 Phone +49-421-218-64226 DFKI GmbH Bremen Fax +49-421-218-9864226 Safe & Secure Cognitive Systems Till.Mossakowski at dfki.de Enrique-Schmidt-Str. 5, D-28359 Bremen http://www.dfki.de/sks/till Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH principal office, *not* the address for mail etc.!!!: Trippstadter Str. 122, D-67663 Kaiserslautern management board: Prof. Wolfgang Wahlster (chair), Dr. Walter Olthoff supervisory board: Prof. Hans A. Aukes (chair) Amtsgericht Kaiserslautern, HRB 2313 From Patrick.Browne at comp.dit.ie Tue Jul 21 12:06:30 2009 From: Patrick.Browne at comp.dit.ie (pat browne) Date: Tue, 21 Jul 2009 11:06:30 +0100 Subject: [Flirts] Dependent types in Institutions In-Reply-To: References: Message-ID: <4A659326.2090909@comp.dit.ie> Introduction I am trying to tease out the differences and similarities between Goguen's concept of dependent types (Goguen 1991) and the concept of dependent types from the Haskell literature (Hallgren 2001),(Hinze, Jeuring et al. 2006). I wish to do this at the level of a worked example. My overall goal is to establish the practical advantages of institution based systems over Haskell's type class mechanism in terms of expressive power and practical use. I am not trying to conduct a theoretical comparison between type theory and institutions. Hence my reasoning must at a practical rather than theoretical level. Because I am trying to establish the practical value of TOI I need a language to language comparison, with the occasional mention of more general concepts. I have chosen CafeOBJ. But my language-to-language comparison really has a more general motivation. It is convenient to have high level concepts that describe both approaches. I use mantras and levels of abstraction to distinguish Haskell and CafeOBJ Mantras Haskell: types as theorems and programs as proof CafeOBJ: types as theories and truth is invariant under change of notation Levels of abstraction Haskell: values < types < classes (Hallgren 2001) CafeOBJ: data elements < data set < concrete algebra < abstract algebra (Goguen 1991) Where Haskell types are sets of values corresponding to CafeOBJ sorts (or Goguen's data sets?). It would appear that Haskell lacks an abstract algebra or theory level. Dependent types in Haskell I am particularly interested in two types 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 Here is a Haskell example from (Raubal and Kuhn 2004). 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) The intended semantics are: 1) Objects have names (or other identifiers) and can be compared for equality using these names. 2) Two objects are considered equal (identical) if they have the same identifier. 3) The type of a name depends on the type of the object, which gets expressed as a type dependency (object -> name). My understanding of Haskell's functional dependency is that | object -> name indicates that fixing the type object should fix the type name. Alternatively we could say that type name depends on type object. The class definition shows a *type-to-type* dependency (object to name), while the instance definition shows how a name value is used to define equality of objects so it is a *value-to-type* dependency (name to object) in the opposite direction to that of the class. ============================================================ Question 1: Is my understanding correct? Question 2: What type of DT is this does this example exhibit? ============================================================== Dependent types in Institution based languages Joseph Goguen also uses the term dependent type (Goguen 1991). I will postpone a detailed discussion of Goguen's paper (it needs more careful study). The module NAMEDOBJECT is my first stab at converting the Haskell definitions above into CafeOBJ module. When the module is opened with actual parameters the variable n1 of type Elt.name is replaced by the actual type that will be used to define the type equality for Elt.object. Elt is the only sort in the TRIV module and represents any set of elements. mod NAMEDOBJECT(object :: TRIV, name :: TRIV) { op name__ : Elt.object Elt.name -> Elt.name -- get name vars o1 o2 : Elt.object var n1 : Elt.name eq name o1 n1 = n1 . eq (o1 == o2) = if (name o1 n1 == name o2 n1) then true else false fi .} We can now open the module with any appropriate types open NAMEDOBJECT(INT,QID) . In the system generated module replaced sorts can be clearly seen. module NAMEDOBJECT(object <= INT, name <= QID) { ** opening imports { protecting (INT) protecting (QID) } signature { op o _ _ : Int Id -> Int { strat: (0 1 2) prec: 41 } op n _ _ : Int Id -> Id { strat: (0 1 2) prec: 41 } } axioms { eq (o o1:Int n1:Id) = o1 . eq (n o1:Int n1:Id) = n1 . eq (o1:Int == o2:Int) = (if ((n o1 n1:Id) == (n o2 n1)) then true else fals fi) . }} =================================================================== Question3: Does this module have *dependent types*? Question4: If so, are they type-to-type or value-to-type? Question5: Is Goguens's idea of dependent type the same, overlaps or disjoint from the two Haskell versions of the term mentioned above. ====================================================================== I appreciate that there are many vague notions here, but any opinions or directions for further study would be appreciated. Best regards, Pat Goguen, J. (1991). Types as Theories. Topology and Category in Computer Science. G. M. Reed, A. W. Roscoe and R. F. Wachter, Oxford University Press: 357-390. 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. Raubal, M. and W. Kuhn (2004). "Ontology-Based Task Simulation." Spatial Cognition & Computation 4(1): 15-37.