Any thoughts on subtyping, type classes and object-oriented encoding?

[paulotorrens]

I'd like to experiment using calculus of constructions as an intermediate language, and I'm particularly interested in compiling Objective-C to it. I might encode statements and side-effects as monads, I don't see any problems for this (yet?), but I'm not sure how one would encode subtyping (or, to be more precise, bounded quantification).

I'd like to start a discussion: how would one encode object-oriented classes, or Haskell's type classes, in CoC? My first naïve idea is to encode those types as sigma-types (dependent pairs), whose first member is the type and the second member is a proof of subtyping, so that I may only instantiate polymorphic functions if I may prove my type parameter to be a subtype of the desired one. What do you think?

Does anyone have any ideas or papers on how to do that?

[Gabriella439]

Probably the easiest way to motivate this discussion is to include some object-oriented pseudo-code that you would like to compile to the calculus of constructions. Then people can propose various ways to encode your example

[VictorTaelin]

For encoding Haskell's typeclasses specifically you can just use dictionaries, here is an explanation from Gabriel.

[paulotorrens]

Hm, interesting idea of using value-level encoding. I wonder if something like that could be encoded at type-level. CoC/Morte has the potential of being used as proof-carrying code, I wanna experiment on that.

For discussion purposes, lets consider the safe and sound parts of Objective-C (no arbitrary pointer casts, etc). For example, this piece of code:

@protocol P // A protocol is Objective-C's equivalent of a Java interface
@end        // I.e., a contract that a class will implement some behavior

@interface A // Some base class A
@end

@interface B: A<P> // Some class B which inherits A and implements P
@end               // I.e., B is a subtype of both A and id<P>

@interface C<P> // Some class C which implements P
@end

void foo(A *a)    { /* ... */ } // Would accept A and B, but not C
void bar(id<P> p) { /* ... */ } // Would accept B and C, but not A

Function dispatch is dynamic, so this is a non-issue. I'm trying to think of ways of encoding foo and bar such that they would only work with respect to subtyping information. As I said, I was thinking of using a proof of subtyping as a parameter to them. So how could I encode classes as types such that I could write a function that has enough information to then compares them?

P.s.: merry Christmas y'all. :smile:

[Gabriella439]

For that specific example, I would encode it as:

$ cat ./P
-- Boehm-Berarducci encoding of the type of an empty record
-- since you gave it no fields or methods
∀(P : *) → P

$ cat ./A
-- Same thing
∀(A : *) → A

$ cat ./B
-- Same thing
∀(B : *) → B

$ cat ./foo
λ(a : ./A ) → ...

$ cat ./bar
λ(p : ./P ) → ...

... and the following subtyping conversions:

$ cat ./bToA
λ(x : ./B ) → x  -- Identity function, since they are identical

$ cat ./bToP
λ(x : ./B ) → x  -- Same thing

$ cat ./cToP
λ(x : ./C ) → x  -- Same thing

... and then if I tried to apply foo to a value of type B in an objective-C-like language:

^(B x) { foo(x) }

... then the underlying encoding would implicitly insert the subtyping conversion:

λ(x : ./B ) → ./foo (./bToA x)