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
    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
    public readonly proof_axiom1:Axiom1    

    Axiom2: \\\etcetcetc

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

  • $\begingroup$ 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. $\endgroup$
    – 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

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

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

    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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.