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$
$\endgroup$
1
-
1$\begingroup$ Can you give a "dependent type declaration" and a "class definition" that you think resemble each other? $\endgroup$– Derek Elkins left SECommented Dec 16, 2017 at 0:10
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
3
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.
answered Dec 16, 2017 at 8:39
-
$\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$ Commented Dec 17, 2017 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$ Commented Dec 18, 2017 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$ Commented Dec 18, 2017 at 12:07