
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