# Curry-howard isomorphism in object oriented programming languages

I want to get a better intuition for the curry howard isomorphism, and my intuition is mainly based on object oriented programming languages like JavaScript.

So as an example, I am going to formalize the notion of "topological space" in a hypothetical object oriented programming language with dependent type theory and see if it makes sense:

public class TopologicalSpace
{
BaseSet:Type
Topology: (BaseSet -> Boolean) -> Boolean
public TopologicalSpace(X:Type,T:(X -> 2) -> 2,
p_axiom1:Axiom,p_axiom2:Axiom2,p_axiom3:Axiom3 )\\constructor
{
BaseSet = X;
Topology = T;
proof_axiom1 = p_axiom1;
proof_axiom2 = p_axiom2;
proof_axiom3 = p_axiom3;
}

Axiom1: Topology (function (x:BaseSet) return True) = True
AND Topology (function (x:BaseSet) return False) = True \\empty set & domain
\\ are in topology

Axiom2: \\\etcetcetc
}


Does this approach make sense? Is there a kind of object oriented type theory + curry howard isomorphism like this?

• You could use that approach, but you'll never be able to run these programs in a meaningful way. Recall that given $f,g:\mathbb N\to 2$ we can't check whether $f=g$ with a program.
– chi
Oct 29 '18 at 12:42

If you only consider terminating functions, then your axiomatisation works :-) Indeed, terminating functions have a resonable notion of equality: If their return type has decidable equality then the functions have decidable equality.

Regarding your code, it could be rendered in an OOP-like fashion this way

record TopologicalSpace : Set₁ where

field
BaseSet  : Set
Topology : (BaseSet → Boolean) → Boolean

Empty    = λ (x : BaseSet) → false
Universe = λ (x : BaseSet) → true

field
axiom1   :       Topology Empty    ≡ true
AND  Topology Universe ≡ true


This is a real programming language whose functions must always terminate: It is Agda; http://learnyouanagda.liamoc.net/

The source for the code can be found here: https://github.com/alhassy/RandomProgramming/blob/master/Agda/TopologicalSpaces.agda