Open bblfish opened 2 years ago
Assuming one found a way of adding a pure definition of a function to the Function Ontology. How would one model Java? The key article to read there is Bart Jacobs's classic 2003 Coalgebras and monads in the semantics of Java - and his earlier articles on OO and colagebras from the 1990s.
The semantis of a statement
public B foo(A x)
is written mathematically as
S × A → Hang + Normal + Abrupt
ie a function that takes a pair of a state and an argument A and returns either a result that specifies the Hanging of the VM or a Normal return value (e.g. B
) or an Abrupt termination given by an exception. Both the exception and the Normal termination return a new state of the VM expressed as
S × A → 1 + (S × B) + (S × E)
a function takes a state and an argument and returns either a singleton (unit) or a new state and the result or a new state and the Exception. Bart Jacobs then shows how one can transform that into a monad view and also into a coalgebraic view. The coalgebraic view is the OO perspective: objects with methods that transform its state.
In §4.1 I read
I think all these are non-controversial, except that a function can have multiple results. So I think this decision needs to be argued for carefully.
Here is the counterargument that would need to be answered: In mathematics (such as category theory) a function is a relation that covers the whole of a domain and has exactly one value for each element of the domain, each of those values being located in the range. We find this in owl, where an
owl:FunctionalProperty
is a relation for any object on which it is defined, has exactly one value.In Category Theory we have the following two categories which are related by 3)
So there are some interesting questions: