Re: [Haskell-cafe] Fwd: representing institutions in haskell

Dear Rick, actually, in the Hets system [1], which is one of the largest Haskell programs, we have represented logics as institutions since 2002. Hets comprises of about 25 logics represented as institutions, including propositional logic, first-order logic, higher-oder logic, modal logic, OWL, and even some functional programming language. Hets provides parsing, static analysis, and proof management for logical theories formulated within these institutions (and also heterogeneous theories spanning several institutions). Interfaces to various theorem provers, SAT solvers and model finders are included. Hets' input language is the Distributed Ontology, Model and Specification language (DOL) [2], which has been standardized by the Object Management Group (OMG). More specifically, Hets employs a type class "Category" for representing categories, with functions for identities, domain, codomain and composition. On top of this, institutions form a multi-parameter type class "Logic", with a representation of signatures and signature morphisms as a category. The set of sentences is represented as one parameter type. This is a pragmatic decision, since in most institutions, sentences are uniform over signatures, and making this dependent on signature would be much more complicated. But many functions on sentences depend on a signature. Sentence translation along a signature morphism is represented by a function of the type class as well. Models and satisfaction are generally not represented due to their (in general) infinitary nature. But in some case, we represent models as certain theories, e.g. when processing the output of some model finder. Such models can even be translated using institution comorphisms. That said, we are interested in improving the representations of institutions in Hets, e.g. by making more using some libraries for category theory that have not been available in 2002 when we started Hets. However, I must admit that I did not understand your representation, Rick. Could you explain its general principles? What is the purpose of having "data Sign a = Sign a"? Why do conjunction and disjunction play such a role, given that there are institutions like equational logic that neither have conjunction nor disjunction? I could I execute your code, neither with ghc 7.6.3, nor ghc 8.0.2. I suggest that you choose some simple logic, like propositional logic, and represent it as an institution in Haskell with your approach. Then we will have a better basis for discussion. Best, Till [1] http://hets.eu [2] http://dol-omg.org Am 17.05.2016 um 14:55 schrieb rick:

Hello Christian:

I thought I should send this to you separately in case you are not on the Haskell list any more.

You may enjoy the samples below which use some standard Haskell libraries that may not have been available when you and Till started work on HETS.

-- Rick

-------- Forwarded Message -------- Subject: [Haskell-cafe] representing institutions in haskell Date: Mon, 16 May 2016 15:13:34 -0400 From: rick To: haskell-cafe@haskell.org

Has anyone here taken an interest in representing institutions [1] in Haskell?

Institutions originated in work on CLEAR [2] which was the first algebraic specification language with rigorous semantics.

Institutions take some time to explain, or unravel if you follow the reference, but they come with a convenient slogan : "Truth is invariant under change of notation."

The stretch goal of institutions is transforming logics while preserving satisfaction.

They are conceived in terms of categorical abstractions, so it's natural to represent them in categories. I hope some folks here find institutions a useful domain to apply their work on categories.

I've attached two samples in Haskell that uses some standard libraries : Arrow, Monad, Category and Dual.

The first sample, ri-0, outlines the essentials. The category of signatures, constructions in the categories, signature morphisms, sentences, models and the satisfaction condition.

Using plain old Nat reduces the complexity of the exposition.

I provide a constructive witness for satisfaction of the morphism from conjunction to disjunction.

You may recognize that I borrow some Bird/Hinze notation on Functors like mapSign. And you find some experiments with Quickcheck and Yampa.

Ri-0 runs from main, but just computes the witness to the satisfaction condition.

The second sample, ri-1, builds on ri-0. Rather than Nat, I use Either to inject disjunction into the exposition. The exposition becomes more complex, but the increased complexity is justified because maintaining satisfaction under change on notation is central to institutions.

The functions prodSum takes conjunction to disjunction and sumProd takes disjunction to conjunction. I owe a citation to @BartoszMilewski and his work on categories for programmers where I first saw these functions.

The satisfaction condition and witness appear more complex in ri-1, but its really just the substitution of the signature morphism on product and sum rather than plain old Nat as in ri-0.

I also plan a better write up, but before I do I expect to learn much from an email exchange with interested folks here.

Thanks for taking a look at this material.

1. https://cseweb.ucsd.edu/~goguen/pps/ins.ps

2. http://hopl.info/showlanguage.prx?exp=945