1
$\begingroup$

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
    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?

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

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

$\endgroup$

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.