snippetMinor
Is it possible to implement dependent types by any object oriented language supporting inheritance and classes?
Viewed 0 times
implementanyandlanguageinheritancepossiblesupportingclassestypesoriented
Problem
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?
Solution
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.
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.
Context
StackExchange Computer Science Q#85556, answer score: 4
Revisions (0)
No revisions yet.