[Haskell-cafe] representing institutions in haskell

[rick]

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

-- 
Rick
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Main.hs
Type: text/x-haskell
Size: 7900 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160516/d3d3d2d5/attachment.hs>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Main.hs
Type: text/x-haskell
Size: 5982 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160516/d3d3d2d5/attachment-0001.hs>