4 ms·

Alright, I can see where you're coming from... I guess it does all get kind of fuzzy once you have a TC type system anyway. (Whether that be via full dependent

Alright, I can see where you're coming from... I guess it does all get kind of fuzzy once you have a TC type system anyway. (Whether that be via full dependent types or the rather strange not-quite-like-working-with-terms-and-types world of not-full-dependent-typing of e.g. Haskell.)

dwohnitmok 8y ago
A Turing-complete type system and a dependent type system are two different and independent things. That is it's possible for a type system to be dependently typed and not Turing complete and it is possible for a type system to be Turing complete and not be dependently typed (even a little bit). Dependent typing concerns whether your types can depend on values. So for example if a then Int else Bool is a (single) dependent type if `a` is a runtime value. The difference between the two can be illustrated with natural numbers with the classic natural-number-indexed vector example that always shows up with dependent typing. If you have a type Vector 5 Character representing a vector of 5 elements of characters, if that 5 is the same 5 as you have at runtime then you have dependent typing. Otherwise this is not an example of dependent types. Put another way, if you're allowed to do something like the following val x: Int = 5 val xs: Vector x Character = Vector('a', 'b', 'c', 'd', 'e') in pseudo-Scala syntax then you have dependent types. If on the other hand you have something like type Zero type One ... type Four type Five ... val xs: Vector Five Character = Vector('a', 'b', 'c', 'd', 'e') where you have a special set of type-level numbers that are distinct from your run-time natural numbers then you have typelevel programming but do not have dependent typing. Your type system might let you do arbitrary things with the type-level natural numbers type Zero type One ... which would mean your type system is Turing-complete even if it's not dependently typed. Note that in practice it's usually true that languages with typelevel programming tend to inch towards dependent types. For example, by allowing val xs: Vector Five Character = Vector('a', 'b', 'c', 'd', 'e') to type-check but not allowing val xs: Vector Five Character = Vector('a', 'b', 'c', 'd', 'e', 'f') to type-check, unless your language is special-casing behavior for collections, there's usually some way to back out some sort of connection between a type-level Five and a run-time 5 (although this connection often only works for numeric literals in e.g. current Scala and works via macros). There's also a considerable amount of social overlap between programmers interested in typelevel programming and programmers interested in dependent types which tends to drive development of language features along those lines. However, in theory, the two are completely separate.
- didibus 8y ago
  I see, so in a way it adds nothing more then convenience? In that, you could manually go ahead and create VectorTwo VectorThree, etc. But no one does because its tedious. So now you could instead say the type is (Vector of Two), which would evaluate to VectorTwo. I'm still unclear how the type system knows that a VectorOne fits in a VectorTwo, and how inference could work at that level. Also, with dependent types, I'm unclear what you mean with runtime values, if its still type checked at compile time, wouldn't the value need to be there at compile time?
  - dwohnitmok 8y ago
    First off, general note to whom it may concern: Down-voting clarifying questions (e.g. the question I'm replying to) seems unhelpful. It is indeed merely syntactic convenience if all you have are the labels type Zero type One type Two ... If however, you have operations on those labels that are checked by the compiler, then you have what most people think of when they say "type-level programming," which is more than a syntactic convenience. For example, if the compiler recognizes addition of type-level numbers, that is there is a notion of Plus so that Plus One Two unifies with Three then all of a sudden you can do the classic length-indexed demo of length-checked append. appendInts: (Vector N Int, Vector M Int) => Vector (Plus N M) Int again in pseudo-Scala syntax, which you can't do with simply labeling VectorOne, VectorTwo, etc. Your question about dependent types is the classic one, if I understand it correctly. Namely, what does it mean for a type (a compile-time concept) to depend on a run-time value, if that run-time value almost always (except for literals) doesn't exist at compile time? The answer is that your type signatures usually end up being generic in the run-time value, and then different code paths allow you to add increasingly specific pieces of information to the run-time value. These code paths are fixed at compile time so the compiler is able to use these pieces of information when it type-checks the code. An example is probably in order. Let's say you're accepting user input in the form of a vector of integers (and let's ignore how we were able to format stdin into a vector for now). Again we'll use pseudo-Scala syntax. val userInput: Vector n Int Note that here `n` is an Int (e.g. a 5) not a type-level Five since we're back in dependent type land. Now we might have a function that only works for vectors of exactly length three and generates some string for those vectors. myFunction: Vector 3 Int => String In order to use `myFunction` on `userInput`, we'll need some intermediate function that actually performs a check that `n` is indeed 3. checkIf3 : (n: Int) => Either[n != 3, n = 3] Now we can do the following. checkIf3(userInput) match { case Right(nWasIndeed3) => // Now the compiler knows that in this code path n is indeed 3 myFunction(userInput) case Left(nWasNot3) => // Throw some error as appropriate } How you actually pass the information in the `Right` branch that `n = 3` to the compiler is implementation specific. Some implementations might decide to special-case equality and have the compiler automatically include that in the compilation process. Others might use some form of implicit arguments to `myFunction` (so that e.g. Vector 3 Int is actually syntactic sugar for (implicit n = 3, Vector n Int)). Hopefully, however, that serves as an understandable overview of what the general approach looks like. Now if you're familiar with statically typed languages, you might rightly point out that what I've done in this example I could've done with just ordinary non-dependent types. E.g. if I used a type-level `n` instead of a runtime `n`. This is true for single-argument functions, but dependent types start pulling ahead in expressivity when you have multiple arguments that are related to one another. For example indexing a vector might look like getElementAtIdx: (Int, Vector n A) => Option[A] in a non-dependently typed language because we don't have a way of expressing a (run-time) relationship between the first and second arguments to our function, namely that the first integer must be less than `n`. With dependent types we can do this by introducing a third argument. getElementAtIdx: (idx: Int, Vector n A, idx < n) => Option[A] Note that we've also added the syntactic ability to bind a type to a variable in a type signature (idx), which is helps us express relationships among different arguments.

dwohnitmok 8y ago

A Turing-complete type system and a dependent type system are two different and independent things. That is it's possible for a type system to be dependently typed and not Turing complete and it is possible for a type system to be Turing complete and not be dependently typed (even a little bit). Dependent typing concerns whether your types can depend on values. So for example if a then Int else Bool is a (single) dependent type if `a` is a runtime value. The difference between the two can be illustrated with natural numbers with the classic natural-number-indexed vector example that always shows up with dependent typing. If you have a type Vector 5 Character representing a vector of 5 elements of characters, if that 5 is the same 5 as you have at runtime then you have dependent typing. Otherwise this is not an example of dependent types. Put another way, if you're allowed to do something like the following val x: Int = 5 val xs: Vector x Character = Vector('a', 'b', 'c', 'd', 'e') in pseudo-Scala syntax then you have dependent types. If on the other hand you have something like type Zero type One ... type Four type Five ... val xs: Vector Five Character = Vector('a', 'b', 'c', 'd', 'e') where you have a special set of type-level numbers that are distinct from your run-time natural numbers then you have typelevel programming but do not have dependent typing. Your type system might let you do arbitrary things with the type-level natural numbers type Zero type One ... which would mean your type system is Turing-complete even if it's not dependently typed. Note that in practice it's usually true that languages with typelevel programming tend to inch towards dependent types. For example, by allowing val xs: Vector Five Character = Vector('a', 'b', 'c', 'd', 'e') to type-check but not allowing val xs: Vector Five Character = Vector('a', 'b', 'c', 'd', 'e', 'f') to type-check, unless your language is special-casing behavior for collections, there's usually some way to back out some sort of connection between a type-level Five and a run-time 5 (although this connection often only works for numeric literals in e.g. current Scala and works via macros). There's also a considerable amount of social overlap between programmers interested in typelevel programming and programmers interested in dependent types which tends to drive development of language features along those lines. However, in theory, the two are completely separate.

didibus 8y ago
I see, so in a way it adds nothing more then convenience? In that, you could manually go ahead and create VectorTwo VectorThree, etc. But no one does because its tedious. So now you could instead say the type is (Vector of Two), which would evaluate to VectorTwo. I'm still unclear how the type system knows that a VectorOne fits in a VectorTwo, and how inference could work at that level. Also, with dependent types, I'm unclear what you mean with runtime values, if its still type checked at compile time, wouldn't the value need to be there at compile time?
- dwohnitmok 8y ago
  First off, general note to whom it may concern: Down-voting clarifying questions (e.g. the question I'm replying to) seems unhelpful. It is indeed merely syntactic convenience if all you have are the labels type Zero type One type Two ... If however, you have operations on those labels that are checked by the compiler, then you have what most people think of when they say "type-level programming," which is more than a syntactic convenience. For example, if the compiler recognizes addition of type-level numbers, that is there is a notion of Plus so that Plus One Two unifies with Three then all of a sudden you can do the classic length-indexed demo of length-checked append. appendInts: (Vector N Int, Vector M Int) => Vector (Plus N M) Int again in pseudo-Scala syntax, which you can't do with simply labeling VectorOne, VectorTwo, etc. Your question about dependent types is the classic one, if I understand it correctly. Namely, what does it mean for a type (a compile-time concept) to depend on a run-time value, if that run-time value almost always (except for literals) doesn't exist at compile time? The answer is that your type signatures usually end up being generic in the run-time value, and then different code paths allow you to add increasingly specific pieces of information to the run-time value. These code paths are fixed at compile time so the compiler is able to use these pieces of information when it type-checks the code. An example is probably in order. Let's say you're accepting user input in the form of a vector of integers (and let's ignore how we were able to format stdin into a vector for now). Again we'll use pseudo-Scala syntax. val userInput: Vector n Int Note that here `n` is an Int (e.g. a 5) not a type-level Five since we're back in dependent type land. Now we might have a function that only works for vectors of exactly length three and generates some string for those vectors. myFunction: Vector 3 Int => String In order to use `myFunction` on `userInput`, we'll need some intermediate function that actually performs a check that `n` is indeed 3. checkIf3 : (n: Int) => Either[n != 3, n = 3] Now we can do the following. checkIf3(userInput) match { case Right(nWasIndeed3) => // Now the compiler knows that in this code path n is indeed 3 myFunction(userInput) case Left(nWasNot3) => // Throw some error as appropriate } How you actually pass the information in the `Right` branch that `n = 3` to the compiler is implementation specific. Some implementations might decide to special-case equality and have the compiler automatically include that in the compilation process. Others might use some form of implicit arguments to `myFunction` (so that e.g. Vector 3 Int is actually syntactic sugar for (implicit n = 3, Vector n Int)). Hopefully, however, that serves as an understandable overview of what the general approach looks like. Now if you're familiar with statically typed languages, you might rightly point out that what I've done in this example I could've done with just ordinary non-dependent types. E.g. if I used a type-level `n` instead of a runtime `n`. This is true for single-argument functions, but dependent types start pulling ahead in expressivity when you have multiple arguments that are related to one another. For example indexing a vector might look like getElementAtIdx: (Int, Vector n A) => Option[A] in a non-dependently typed language because we don't have a way of expressing a (run-time) relationship between the first and second arguments to our function, namely that the first integer must be less than `n`. With dependent types we can do this by introducing a third argument. getElementAtIdx: (idx: Int, Vector n A, idx < n) => Option[A] Note that we've also added the syntactic ability to bind a type to a variable in a type signature (idx), which is helps us express relationships among different arguments.