[Haskell-cafe] Fwd: representing institutions in haskell

[Till Mossakowski]

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 <rick at rickmurphy.org>
> To: haskell-cafe at 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
>