“Perfection is achieved not when there is nothing left to add, but when there is nothing left to take away” (Antoine de Saint-Exupéry)
--
The semantic function in DDWTCM & DDFMTP papers, ⟦_⟧, μ, decribes a mapping from a Syntactic Doman → Semantic Domain
"Denotational semantics is a compositional style for precisely specifying the meanings of languages,
invented by Christopher Strachey and Dana Scott in the 1960s
The idea is to specify, for each syntactic category C,
• a mathematical model ⟦C⟧ of meanings, and
• a semantic function ⟦_⟧ :: 𝒞 → ⟦𝒞⟧
Similarly, we can apply denotational semantics to data types within a language to give precise meaning, independent of its implementation."
"For a language, the meaning function is defined recursively over the abstract syntactic constructors. This practice transfers directly to algebraic data types."
The motivation behind denotational design, is to formalize the principles of representation hiding, and the algebraic program design.
"Denotational Design from meanings to programs" Conal Elliot@LambdaJam Design methodology for “genuinely functional” programming: Precise, simple, and compelling specification. -Informs use and implementation without entangling them. Standard algebraic abstractions. -Free of abstraction leaks. -Laws for free. -Principled construction of correct implementation. """ The distinction between algebraic and denotational design, lies along the levels at which each takes place. while both necessarily pertain to the design of code objects, denotational design more specifically pertains to the processes of abstraction and abstraction mapping, i.e. the essence of types, "What do these operations ... types mean" while algebraic design pertains to implementation patterns of programs, i.e. operations on types "What is an algebra for an api" [where algebra: sets/types, operations on sets/functions, laws]
DDTCM - on a particular example of maps "" The type is abstract, available only through an explicit interface that does not reveal its representation. A central question is “What does a map mean?” In other words, “A map is a representation of what mathematical object?” ""
Type class morphism principle
"""
The instance's meaning follows the meanings instance
That is, the meaning of each method application is given by application of the same method to the meanings of the arguments.
In more technical terms, the semantic function is to be a type class morphism, i.e. it preserves class structure.
"""
Implementations of type class instances can sometimes be derived mechanically from desired type class morphisms.
Suppose we have ⟦·⟧ :: T → T′ , where T′ belongs to one or more classes and ⟦·⟧ is invertible.
Then, combining ⟦·⟧ and ⟦·⟧^1 gives instances that satisfy the morphism properties
Following through
-- 'Rig Overloading'
--
"[...]Try giving your library/DSL more than one denotation, perhaps of overlapping subsets of your full vocabulary. Give each "language" subset as simple a denotation/interpretation as you can. Each denotation brings its own notion of equality (i.e., having equal denotations), and you can state and prove laws in terms of these equalities. In particular, look for laws in the form of type class morphisms, guided by the type classes inhabited by your (as simple as possible, while precise & adequate) denotations. Rather than discarding denotation (or implementation-independent specification in general), apply it more finely. More denotations, not fewer."
- Conal elliot reddit thread comments reacting to criticism of denotational design
"This sort of feels like sheaf semantics" "I started to get the hunch that if you really formalized the approach it would look a lot like that -- in particular we treat the "type class morphism" of denotation as a functor, substitute Hask for Set, and we're off to the races. ... [ To continue further here, look at the running examples of e.g. pictures as "location -> color" and reactive programming as "time -> value"
add in some continuity conditions and bear in mind you need to flip the arrows because contravariant functor and it looks a lot like a sheaf! ]"
"Sheaves can be defined over a base category which has a system of covering families which satisfy certain axioms we think of a typeclass morphism as just a mental model of a "semantics functor"
Extending the semantic function, to a semantic functor, (or more specifically a semantic presheaf) toward sheaf semantics of denotational design
Need categorical formulation of sheaves in terms of epimorphisms
recalling functors, { F G, ... }, between categories { C, D, ... }
functors map objects { a,b,c,... : Obj(C) }, and morphisms { f, g,... : Hom(C) }, of the domains, to objects and morphisms F(a): D, F(f): D
in their codomain
contravariant functors map objects and morphisms of the oppsite category C˚ to a Category D,
while objects are the same between a category and its dual, or opposite, the direction of arrows is reversed,
making f: A -> B in C, f˚: B -> A in C^-1
in the notation of a programming language
haskell
class Functor f where
map :: (a -> b) -> f a -> f b
laws:
map id x = x
map (f · g) = (map f) · (map g)
class ContravariantFunctor f where
contramap :: (b -> a) -> f a -> f b
laws:
contramap id x = x
contramap (f · g) = (contramap g) · (contramap f)
trait Functor[F[_]] {
def map[A, B](f: A => B): F[A] => F[B]
}
trait ContravariantFunctor[F[_]] {
def contramap[A, B](f: B => A): F[A] => F[B]
}
then
trait Presheaf[F[_]] {
def restriction[U, V](f: V => U): F[U] => F[V]
}
def (f|V)[U, V]: F[U] => F[V] = Presheaf[F].restricion(f) // where f: V => U
// written f|V, elements F[A] are called sections
Monomorphisms ~ Embeddings ~Set (Injections ~ Left Total Functions)
Epimorphmisms ~ Coverings ~Set (Surjections ~ Right Total Functions)
Isomorphisms ~ Weak Equality ~Set Bijections ~ One to One mappings
Sites: a site is a small category equipped with a coverage
A coverage on a category C consists of,
for each object U ∈ C, a collection of families { fi : Ui → U }i ∈ I
of morphisms with target U to be thought of as covering families.
Covering Conditions
A coverage on a category C
consists of a function assigning to each object U ∈ C
a collection of families of morphisms { fi : Ui → U}i ∈ I, called covering families, such that
If { fi : Ui → U }i ∈ I is a covering family and g : V → U is a morphism,
then there exists a covering family { hj : Vj → V } such that each composite ghj factors through some fi.
∃: Vi → Uj
fi: Uj → U
hj: V1 → V
∀g: V → U
fi · ∃ = ∀g · hj
Goal:
Where Syn_L Syntax Category over {objects are terms in L morphisms are term mappings} a language L, Sem_L' is a Semantic Category
prove ⟦_⟧: Syn -> Sem
is a Presheaf ~ Sem is a small category, is a contravariant functor from Syn˚ to Sem
is a Sheaf ~ Has satisfactory covering