Talk:Dependent type

Questions

Formal definition

First, a proposed clarification designed to formalize introduction of the term "term":

Let A be a type in a universe U of types. The members a : A are "terms." Now consider a _family of types_ B : A -> U that [sic] assigns to each term a in A a type B(a) in U.

now the question:

B is a function from A to U. Its co-domain, U, does not vary depending on its argument. Its co-domain is the constant collection U, the Universe of types. As I read this, then, B cannot be "a function whose co-domain varies depending on its argument." Could B(a), the value of function B given a term a, itself be "a function whose co-domain varies depending on its argument?" The value B(a) is a type u in U, and a type $B(a) = u \in U$ could be "a function whose co-domain varies depending on its argument." If so, then types u in U are functions whose co-domains vary depending on their arguments, but now I'm confused: what are the domains and co-domains of types u in U if they are functions whose co-domains vary depending on their arguments?

I'd be grateful for clarification of this paragraph. It doesn't parse easily, and I don't know enough, personally, to resolve the questions.

EDIT: I got some clarity here that the authors of this page might want to consider: http://math.stackexchange.com/questions/1119131/basic-definition-of-dependent-types — Preceding unsigned comment added by Rebcabin (talk • contribs) 18:36, 25 January 2015 (UTC)

Ada2012

Is Ada really dependently typed? — Preceding unsigned comment added by Greg greggory (talk • contribs) 00:07, 23 September 2022 (UTC)

Untitled

The Type system article describes dependent types as "types which depend on run-time values". This is obviously a computer science oriented definition, but would it be useful to add it to this article? --65.147.3.110 20:08, 10 September 2006 (UTC)

there should also be something about the berendregt cube, \lambdaP, and the relation to other type systems

there should be information about implementation difficulty, undecidability, etc.

Coq is actually based on the Calculus of Constructions (a.k.a. Lambda P Omega), which is a strictly more powerful system than Lambda P. In the traditional orientation of the Barendregt cube, Lambda P forms the front, bottom, right corner, and CC the back, upper, right corner (which corresponds, relative to Lambda P, to the addition of terms depending on types (as in System F) plus types depending on types (as is Lambda Omega / System F Omega)).

C++ templates

I added C++ templates to the list of supporting languages. I am not sure if this is in accordance with the definition of dependent types, but I decided to wp:be bold. Here is a basic example of an array in C++:

template <class T, int i>
class array {
public:
  T elements[i];
};

array<char, 5> foo; // array of 5 char's

--Spoon! (talk) 01:48, 6 December 2007 (UTC)

I reverted the above; it's a reasonable example of parametrized types but dependent types literally means that the types depend on terms that are passed around as values (as function args, etc). The closest thing you'll find to it in a more or less mainstream language is GADT's in Haskell. The description in the article is a bit incomplete and I'll try to fix it. The key point is that dependent types are fully checked by the compiler, so if you have a type corresponding to an array of 5 chars, then using a term like x[k] will result in a compile time type error unless the compiler can statically guarantee that k is less than 5. That allows writing programs that are provably free of out-of-range subscripts, without needing any runtime checks. You can encode more complex properties as types as well. For example, you could have a type for prime numbers. A term with that type could then never have a composite value, since the program would fail to compile if it created any possibility of the value being composite. Languages with features like this are closely related to proof assistants. 207.241.239.70 (talk) 18:26, 21 November 2008 (UTC)

I tried adding a little more exposition; I hope it helps. 207.241.239.70 (talk) 09:24, 22 November 2008 (UTC)

Arbitrary bounds checking for any static array type is impossible. Think of a program, which accesses a certain array index, after an arbitrary other program halted or which generates an out-of-bounds index only in that case. If a dependent type requires decidability of out-of-bounds accesses, no programming language could ever support dependent types. Templates, like those in C++, indeed create a type that is bounds-checked as far as C++ static bounds checking goes. The template's type is known at compile-time and depends on the argument. But it will only allow compile-time constants as template arguments. That's the point. If I understand right, a dependent type in practice should allow for variable (non-constant) template arguments, something like if there would be a type of C++ templates. It may try to verify them at compile-time for correctness (which might not always make sense). Particularly, if a runtime input is used as array-length and as indices, it cannot decide the occurence of out-of-bounds accesses statically. Runtime checks are required for any language to prevent out-of-bounds accesses because of non-deterministic input. If we are looking in classic languages, I would imagine a switch-case statement to be the closest candidate for an (inlined) dependent function if we consider processing the return value directly in the switch-statement itself. Otherwise, input-dependent output types are rather to be found in dynamically typed languages. Dynamic member fields which contain a type (for example represented as JavaScript constructor function) can be considered to depend on the object which contains them, dependent types. As dynamically typed languages, they usually just don't bother verifying the consequences even though they could. Typescript is closer to it. 2001:16B8:C227:1800:B9CB:6B3F:934D:9A89 (talk) 03:48, 14 February 2022 (UTC)

Other Dependently Typed Languages

Probably a section on languages that support a subset of dependent types such Haskell with GADTs, Omega, Beluga, or Elphin/Delphin(?) may be worth mentioning. —Preceding unsigned comment added by 94.173.19.247 (talk) 10:14, 10 February 2011 (UTC)

Be WP:BOLD. Tijfo098 (talk) 19:59, 12 April 2011 (UTC)

Is Haskell dependently typed?

In Haskell extended with Rank2Types or ExistentialQuantification you can create types depending on values. Type-level programming libraries in Haskell often provide a function called "reify" for this purpose. Nevertheless Haskell is usually not called "dependently typed". What is the difference between the dependency of types on values described here and the one that (extended) Haskell provides? HenningThielemann (talk) 13:23, 15 April 2013 (UTC)

Could you give an example of how those extensions allow types to depend on values? In forall a. F a, a is always a type, it is never a value. Rightfold (talk) 21:29, 28 March 2019 (UTC)

I believe I know what technique is being talked about, and it is a terrible hack. I think it works roughly like this:

class Reified (ty :: Type) (name :: Type) where
    getReified :: ty -- in ye olden days, you'd add a Proxy name argument; now we have TypeApplications

newtype NeedReified ty name ret = NeedReified { applyReified :: Reified ty name => ret }
-- the unholy sauce              v  higher ranked here  v
reify :: forall name ty r. ty -> (Reified ty name => ret) -> ret
reify value needs = unsafeCoerce (NeedReified needs) value

The idea is that GHC represents values-with-context, of type Ctx => t, as functions D:Ctx -> t, where D:Ctx is a some internal name for the "dictionary" of Ctx, a data structure containing the implementations of the class methods. If a class has only a single method, like Reified, then it is represented as that method. So, the reify's Reified ty name => ret argument is represented by a function ty -> name. The function needs to be stuffed into a newtype wrapper to prevent GHC from attempting (and failing) to discharge the constraint, and then unsafeCoerce is used to smash through all the abstractions to get to the implementation details of GHC, allowing us to masquerade a value of ty as context of Reified ty name. In the block now guarded by reify, the type name can be thought to represent some value of type type. As you might guess, this is really a huge pain to use. This technique is rather old and I've never really seen anyone use it.

However, modern Haskell is probably more dependently typed than ever. With the technique of singletons, Haskell should be able to do anything e.g. Idris can. Yes, it requires a lot of explicit micromanagement, but all the micromanagement is really just explicitly stating how much type erasure should be allowed. Howtonotwin (talk) 21:21, 14 April 2019 (UTC)

Some changes

I heavily edited the introduction, to try to make it readable to a wider audience. I added some history. Hopefully, I didn't introduce any errors.

This page is still shared by type theory and type systems. Those two topics split into separate Wikipedia pages while ago, but still overlap in some areas, like this one. I tried to make that clear. It can certainly be made more clear below with the comparison of programming languages.

I will probably do further editing. "Dependent Type" to me is a general heading that includes both dependent functions (Pi-types) and dependent pairs (Sigma-types). The current page makes it feel like the name only applies to functions and that pairs are its weird evil cousin that don't deserve their own page. Maybe we should create pages for each?

Mdnahas (talk) 17:25, 5 August 2013 (UTC)

Blacklisted Links Found on Dependent type

Cyberbot II has detected links on Dependent type which have been added to the blacklist, either globally or locally. Links tend to be blacklisted because they have a history of being spammed or are highly inappropriate for Wikipedia. The addition will be logged at one of these locations: local or global If you believe the specific link should be exempt from the blacklist, you may request that it is white-listed. Alternatively, you may request that the link is removed from or altered on the blacklist locally or globally. When requesting whitelisting, be sure to supply the link to be whitelisted and wrap the link in nowiki tags. Please do not remove the tag until the issue is resolved. You may set the invisible parameter to "true" whilst requests to white-list are being processed. Should you require any help with this process, please ask at the help desk.

Below is a list of links that were found on the main page:

• http://guru-lang.googlecode.com/svn/branches/1.0/doc/book.pdf

  Triggered by \bguru\b on the local blacklist

If you would like me to provide more information on the talk page, contact User:Cyberpower678 and ask him to program me with more info.

From your friendly hard working bot.—^{cyberbot II}_{Talk to my owner:Online} 00:24, 14 August 2015 (UTC)

Programming Languages in the 1930's

"In 1934, Haskell Curry noticed that the types used in mathematical programming languages followed the same pattern as axioms in propositional logic." How could anyone notice something about mathematical programming when one assumes such things didn't exist in the 1930's since computers didn't exist. The link to Curry's bio says he formulated one of the first programming languages in the 1940's. The Curry-Howard correspondence page notes: "the observation in 1934 by Curry that the types of the combinators could be seen as axiom-schemes for intuitionistic implicational logic" https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Origin.2C_scope.2C_and_consequences Which I assume is predecessor to any observation about mathematical programming language. This could be a product of the rewrite mentioned above. — Preceding unsigned comment added by 73.15.40.2 (talk) 08:42, 26 November 2015 (UTC)

You won me to post this comment.

Either the date is wrong or by "mathematical programming languages", should say the typed lambda calculus or it's combinatory logic counterpart.

The almost 1931 concurrent discoveries by Gödel, Turing-Post and Curry-Church-Shoenfinkel, points that the second phrase is what should be changed, not the date.

For that reason, I will change the part of programming languages for the more precise mention of which ones. — Preceding unsigned comment added by 189.178.42.144 (talk) 20:38, 28 December 2015 (UTC)

Perl 6, Sage, Runtime Verification

I added Perl 6, but now I'm having second thoughts. Perl 6 isn't able to do as much compile-time checking as some of the others, building instead on runtime type checking when arbitrary constraints are involved. I see that Sage (which is on the list) works the same way, albeit with more compile-time checks possible. I'm OK with them (both Perl 6 and Sage) being on the list because the runtime safety appears to be equivalent, but I also want the page to be accurate, but don't know if they should be removed on some compile-time-only technicality. Awwaiid (talk) 02:04, 10 March 2016 (UTC)

Perl 6 type checking is extremely limited and ill-specified. It doesn't have dependent types. See also the section on C++ on this talk page. Rightfold (talk) 12:02, 21 September 2016 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified 2 external links on Dependent type. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20091229234011/http://guru-lang.googlecode.com/svn/branches/1.0/doc/book.pdf to http://guru-lang.googlecode.com/svn/branches/1.0/doc/book.pdf
• Added archive https://web.archive.org/web/20110716082621/http://www.cs.st-andrews.ac.uk/~eb/drafts/ifl08.pdf to http://www.cs.st-andrews.ac.uk/~eb/drafts/ifl08.pdf

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 02:59, 9 September 2017 (UTC)

Universe Polymorphism

I think it would be useful to add a column on whether or not languages with dependent types have universe polymorphism, i.e. the rule

${{\Gamma \vdash T:{\mathcal {U}}_{i}} \over {\Gamma \vdash T:{\mathcal {U}}_{i+1}}}$

Along with typical ambiguity, this feature is important for working with "large" types, especially for encoding category theory. It is featured in Coq and Agda. Any opposed? siddharthist (talk) 20:11, 10 November 2017 (UTC)

Error (dependent and polymorphic types mixed up)

"Polymorphic functions are an important example of dependent functions, that is, functions having dependent type. Given a type, these functions act on elements of that type (or on elements of a type constructed (derived, inherited) from that type)."

I suggest the sentences should be deleted (and maybe also the next one). Polymorphic functions do not have to have dependent types. The second sentence may be right but is out of place. I suppose "Polymorphic functions are functions that, given a type, act on elements of that type (or on elements of a type constructed (derived, inherited) from that type). A polymorphic function returning elements of type C would have a polymorphic type written as.." would be correct but I'm not sure it would fit into the article — Preceding unsigned comment added by Jaam00 (talk • contribs) 18:22, 25 September 2018 (UTC)

Confusion between dependent types and constant values in types

There seems to be some confusion between dependent types and constants in types, not just on this talk page but generally in discussions on the Internet. The article should probably have a section that clarifies this distinction.

Consider the fundamental difference between the following zip functions in Idris and C++:

Vect : Nat -> Type -> Type
zip : (n : Nat) -> Vect n a -> Vect n b -> Vect n (a, b)

template<unsigned N, typename T>
class Vect;

template<unsigned N, typename A, typename B>
Vect<N, pair<A, B>> zip(Vect<N, A>, Vect<N, B>);

It is not just a matter of allowing runtime values or not, but more fundamentally that types may be parameterized over terms in a lower universe (values), even if those terms are not constants. And DTs allow for reasoning based on properties of those values (e.g. a + b ≈ b + a therefore Vect (a + b) A ≈ Vect (b + a) A), rather than just on concrete values (a and b may not even be known constants; yet a + b is a term of type Nat).

As part of this proposed section, there should be a clear definition of "value" which currently seems to be missing from the article. And also a clearer definition of "depends" should be in the introduction.

Rightfold (talk) 14:19, 25 March 2019 (UTC)

Fair criticism

"Well, the article opens with lambda cubes, which sound like some type of sheep meat to me. Then it goes on to discuss λΠ2 systems, and as I don't speak alien I skipped that section. Then I read about the calculus of inductive constructions, which incidentally seems to have little to do with calculus, heat transfer, or construction. After giving a language comparison table, the article ends, and I am left more confused than when I got to the page. – Nick Feb 19 '12 at 5:50" - https://stackoverflow.com/questions/9338709/what-is-dependent-typing#comment11799250_9338709

I came here to understand dependent types. This article did not help.

--Spdegabrielle (talk) 14:35, 14 October 2021 (UTC)