When I was reading Agda tutorial, I noticed resemblance between dependent type declarations and class definitions which I've been primarily used to work with. I'm not totally sure how much sense this questions makes, but what is the real practical difference between types and classes? Could we very well use object oriented approach to define types, and thus construct proofing system similar to Agda by any language supporting class and object construction?

  • $\begingroup$ Can you give a "dependent type declaration" and a "class definition" that you think resemble each other? $\endgroup$ – Derek Elkins Dec 16 '17 at 0:10

So, things like this are possible, but the usefulness varies depending on your system.

First, you can absolutely model object oriented programming in a functional, formal setting. System F-sub is the classic example of this, but Scala Dependent Object Types are another model.

Secondly, let's talk about the difference between types and classes, without dependent types. A class is essentially just a type, combined with a bunch of methods that operate on that type. Classes can be modeled with recursive record types in some languages. The algebraic data types you see in languages like Haskell and Agda are kind of like regrouped classes. An interface groups functions together, and the type specific implementation of those functions for specific classes are spread out. Conversely, algebraic data types group all the variants of a type together, but the different functions are spread out, with each function specifying how it is implemented for each type.

Finally, how do dependent types play into all this? Well, Agda and other Dependent Type languages have a particular feature, namely that types can be indexed by values, and that types are themselves values. Computation can happen not just in expressions, but in types.

Java, Haskell, and every other mainstream language are weaker than this, since their types can't be indexed by arbitrary values. This is what the dependent in dependent types means, and it's what makes them useful for proving things.

To have dependent object oriented types, you need to overcome a few hurdles. One is, do you have mutation, and how does it affect dependent types? Can types refer to mutable variables, or alter state? How is that possible, when type computation happens at compile time, not runtime?

And then you need to decide whether you want to prove actual theorems in your language. Most OO languages are Turing Complete, meaning that the would be inconsistent if interpreted as a logic. This doesn't mean that Dependent types are useless, you can still enforce sophisticated program invariants using them. But Agda and the others feature termination checkers that make them Turing Incomplete.

  • $\begingroup$ What does it mean that types can be indexed by arbitrary values? Objects constructed from classes are quite arbitrary also and indexed so that we can access them by variable name reference, AFAIK. $\endgroup$ – MarkokraM Dec 17 '17 at 8:04
  • $\begingroup$ @MarkokraM Maybe mentally replace "indexed" with "parameterized". Java, for example, does not let you write something like int[] xs = {1,2,3}; Foo<xs> foo = new Foo<xs>(); In Agda, you can. In fact, there is no difference between a type parameter and any other kind of parameter. (Within the context of dependently typed programming, there actually is a distinction between the terms "indexed" and "parameterized" but that's perhaps a bridge for another time.) $\endgroup$ – Derek Elkins Dec 18 '17 at 11:48
  • $\begingroup$ @DerekElkins Got that. I was asking OP also because if I could represent dependent types by common classes, then it wouldnt be much effort to use a lisp like language supporting macros, to implement the whole thing, syntax wide, by that language. $\endgroup$ – MarkokraM Dec 18 '17 at 12:07

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.