docs: started work on a type reference by wizard7377 · Pull Request #3590 · idris-lang/Idris2

wizard7377 · 2025-08-05T21:43:34Z

Description

Created a reference for types

wizard7377 · 2025-08-06T01:23:05Z

Made some preliminary changes

joelberkeley · 2025-08-06T21:49:56Z

+Auto implicits are most useful in proofs, where they differ from regular implicits by irrelevance.
+That is, a regular default will never initiate *anything* that cannot otherwise be initiated, while an ``auto`` default will not change anything outside of the input that cannot be initiated.
+
+For instance, if we want to automatically pass a proof through some functions, we use ``auto`` defaults.


Suggested change

For instance, if we want to automatically pass a proof through some functions, we use ``auto`` defaults.

For instance, if we want to automatically pass a proof through some functions, we use ``auto`` implicits.

andrevidela

I skipped the middle because I thought this would be quick but I spent way longer than I thought. There is enough to work with before tackling the middle anyways

andrevidela · 2025-08-07T21:53:44Z

+Implicits
+^^^^^^^^^^^^^
+
+Implicit function types, those where the value of a parameter can be inferred from the context, can take three forms.


Suggested change

Implicit function types, those where the value of a parameter can be inferred from the context, can take three forms.

Implicit arguments, can take three forms.

andrevidela · 2025-08-07T21:55:48Z

+The first of these, ``{x : A} -> B``, forms the basis "basic" implicit types.
+That is, ``x`` should be inferred *syntactically*.


Suggested change

The first of these, ``{x : A} -> B``, forms the basis "basic" implicit types.

That is, ``x`` should be inferred *syntactically*.

The first one, ``{x : a} -> b`` is the most basic form of implicit arguments, that is

``x`` should be inferred *syntactically*.

andrevidela · 2025-08-07T21:56:42Z

+Implicit function types, those where the value of a parameter can be inferred from the context, can take three forms.
+The first of these, ``{x : A} -> B``, forms the basis "basic" implicit types.
+That is, ``x`` should be inferred *syntactically*.
+This is the equivalent of implicit ``forall`` in Haskell or Rocq, where we might state that ``vectorMap`` on a vector might be:


We should add a footnote here pointing people toward the difference between polymorphism and dependent types. I don't think it belongs in this document as a paragraph but it should probably be mentionned somewhere

andrevidela · 2025-08-07T21:57:13Z

+
+    vectorMap {n = m} f v
+
+These two examples show the power of Idris implicits: while they can be inferred by the compiler, if necessary (or desired) they may be specified by the user


Suggested change

These two examples show the power of Idris implicits: while they can be inferred by the compiler, if necessary (or desired) they may be specified by the user

These two examples show the power of Idris implicits: while they can be inferred by the compiler, if necessary (or desired) they may be specified by the user.

andrevidela · 2025-08-07T21:58:06Z

+Idris has *two* additional modifiers of implicits, however.
+The first, while not that important to the type system of Idris, is *incredibly* useful, and it is the default implicit.


Suggested change

Idris has *two* additional modifiers of implicits, however.

The first, while not that important to the type system of Idris, is *incredibly* useful, and it is the default implicit.

The second form of implicits arguments is the default implicit.

andrevidela · 2025-08-07T22:34:52Z

+The other way to define top level types, ``record``, is documented in detail on the `records`_ page.
+
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Existentials in Types


Suggested change

Existentials in Types

Inferable Placeholders

I don't know what to call this class of terms but existential is extremely confusing because there is already something called existential types in programming and it's not what is exposed here. Existential types are usually an encoding of sigma-types for languages without dependent types.

andrevidela · 2025-08-07T22:39:30Z

+While not restricted to types, existentials are so prevalent within types that there usage bears mentioning.
+Existentials are always of the form ``_``, ``?`` or ``?NAME``, where ``NAME`` is a valid name.
+Named existentials are scoped by *module*, however, they may only exist in one term.


Suggested change

While not restricted to types, existentials are so prevalent within types that there usage bears mentioning.

Existentials are always of the form ``_``, ``?`` or ``?NAME``, where ``NAME`` is a valid name.

Named existentials are scoped by *module*, however, they may only exist in one term.

There is a class of expression that allow to call directly into Idris's inference machine, they are ``_``, ``?`` and ``?identifier``, where ``identifier`` is a valid variable name.

``_`` tells the compiler to wait for this expression to be resolved by another constraint, this is like a normal implicit argument.

``?`` tells the compiler to try to guess what the value is, this is like an auto-implicit.

``?identifiers`` is a **hole**. It allows you to query the type of the value at that point in the program.

I don't think ? is like an auto-implicit (you need %search for that). I'm pretty sure it's solved by inference. The difference between _ and ? is that ? can be solved later. If you use _ in a type signature it's an error if it is not solved at the end of a signature. If you use ?, it can be solved later in the file. (An error if not solved by the end of the file.)

andrevidela · 2025-08-07T22:39:51Z

+
+.. caution::
+
+    Existentials are scoped over modules.


Suggested change

Existentials are scoped over modules.

Holes are scoped over modules.

andrevidela · 2025-08-07T22:41:11Z

+These can occur in types, although typically occur in generated ones.
+Most often, this will occur in usages of generic types, where, for instance, given ``show : {a : Type} -> Show a => a -> String``, we transform the context ``show : {a : Type} -> Show a => a -> String, y = show x |- y : String`` to ``x : ?a, Show ?a |- y : String`` [#f2]_ .
+
+``?`` is similar except, while if ``?a``` cannot be inferred it is made it a typed hole, if ``?`` cannot be inferred, it raises an error


Suggested change

``?`` is similar except, while if ``?a``` cannot be inferred it is made it a typed hole, if ``?`` cannot be inferred, it raises an error

? is completely different as it infers a value in addition to the type. Holes only infer the type.

andrevidela · 2025-08-07T22:42:24Z

+Named existential forms an equivalent to "typed holes", that is, a value to be filled in later.
+These can occur in types, although typically occur in generated ones.
+Most often, this will occur in usages of generic types, where, for instance, given ``show : {a : Type} -> Show a => a -> String``, we transform the context ``show : {a : Type} -> Show a => a -> String, y = show x |- y : String`` to ``x : ?a, Show ?a |- y : String`` [#f2]_ .


I think this needs to be reworked in light of the previous changes

andrevidela

Okay I've only gone through a little bit of this but looking a the overall document I wonder where in the documentation this would fit.

it's definitely not a reference document, it's more like an informal beginner tutorial.
It also repeats information that's already in the idris crash course but in a less structured way, that's not bad in itself but it makes it hard to categorise. It also seems to be aimed at beginners but also makes references to and assumes Haskell knowledge which is already a small niche and it already addressed by the crash course. Finally, it contains many more things than types such as interfaces, quantities and holees.

My suggestion is that this should be broken down into a smaller document that would sit in front of the crash course and would be something like "an idris overview in 5 minutes" and that would allow to talk about all the different topics with only surface-level detail.

Another option would be to keep the same audience, surface-level interest people with some FP experience, and expand it into an actual tutorial,but that's a lot more work so I do not suggest it

what do you think?

andrevidela · 2025-08-14T09:31:49Z

+In addition, to do simple universal quantification, one can write ``forall x . a``, where ``x`` must be only a name (it can't have a type qualifier).
+This is desugared to ``{0 x : _} -> a``.


This should be moved to the next section, we haven't introduced implicits or quantities yet so there is no point in writing down what the desugaring is. Also there is no universal quantification in Idris although there is a forall keyword, calling it that might be misleading.I'll let you judge how to rephrase that,maybe there is another sentence that also uses the phrase "universal quantification" that isn't suggesting Idris has universal quantification

andrevidela · 2025-08-14T09:40:30Z

+    Holes are scoped over modules.
+
+Named holes occur most often in the context of type inference.
+Most often, this will occur in usages of generic types, where, for instance, given ``show : {a : Type} -> Show a => a -> String``, we transform the context ``show : {a : Type} -> Show a => a -> String, y = show x |- y : String`` to ``x : ?a, Show ?a |- y : String`` [#f2]_ .


I don't think the example is very insightful if all the steps are skipped. It's also a lot to introduce new syntax 90% of the way through the document

andrevidela · 2025-08-14T09:43:13Z

+    In addition, this means that one can have anonymous instances, so, for instance, ``Monad (\x => x)`` is a perfectly valid form.
+
+    Even so, it is in general not a good idea to create such instances


Suggested change

In addition, this means that one can have anonymous instances, so, for instance, ``Monad (\x => x)`` is a perfectly valid form.

Even so, it is in general not a good idea to create such instances

If it's not a good idea to do it, we should not encourage users to do it

andrevidela · 2025-08-14T09:43:37Z

+The two main ways to declare types at the top level are ``record`` and ``data``
+
+.. note::
+    Type synonyms, type families, and the like from Haskell are all just normal functions from ``Type`` to something else.


Suggested change

Type synonyms, type families, and the like from Haskell are all just normal functions from ``Type`` to something else.

Type synonyms, type families, and the like from Haskell are all just normal functions ``Type -> a``

Actually, aren't these functions that result in a type? For instance, a type synonym is just

Label : Type Label = String

Same for type families? In fact, we hardly ever write functions of the type Type -> a.

Type families both result in a type (kind) and depend on types given as argument, I've put a because you could be working with multiple kinds not just *. open type families is closest to pattern matching on types, data families are like an indexed interface a -> Type. None of those comparaisons actually make any sense if you think too hard about it. Maybe the paragraph should be scraped because there isn't much pedagogical benefit in relating dependent types to haskell-specific features that don't quite match

andrevidela · 2025-08-14T09:44:43Z

+To declare (Agda style) Generalized Algebraic Data Types, we must write ``data NAME : KIND where CONS``.
+``KIND`` must be a kind (in Idris there isn't actually distinction between types and kinds) whose tail ultimately ends up returning the type ``Type``.


There are no kinds in Idris those are types

andrevidela · 2025-08-14T09:47:37Z

+
+    Even so, it is in general not a good idea to create such instances
+
+``data`` declares (General) Algebraic Data Types ((G)ADTs).


Suggested change

``data`` declares (General) Algebraic Data Types ((G)ADTs).

``data`` declares (Generalized) Algebraic Data Types ((G)ADTs).

a bit weird to call them that because there is no difference between normal data types and gadts in Idris. I would reformulate as "data can also declare types with indicies, that is, where the parameter is a value that can vary depending on the constructor used."

It's actually the other data that's a special compiler case and it desugars to a data type with constant indices

andrevidela · 2025-08-14T09:49:27Z

+In addition, each ``ALT`` must be of the form ``CONS PARAMS`` where each ``CONS`` is either an operator or a name (that will be declared as a constructor).
+Finally, each of ``PARAMS`` must be a valid type.
+
+To declare (Agda style) Generalized Algebraic Data Types, we must write ``data NAME : KIND where CONS``.


Saying that adga has gadts is also weird to me. adga has indexed types and you can use them to write down parameterised data types. it's only haskell that works the other way around

Yeah, I know there are people (see Conor's recent mastodon post) get offended if you refer to an indexed inductive type as a GADT.

I found the post, quite amusing for us. Not amusing for them

wizard7377 · 2025-08-14T19:07:26Z

Probably a quick start at the beginning of the tutorial. I don't think there's an equivalent of that yet and that does seem rather important, so I'll get to work shortening it and adding the rest of basic Idris

wizard7377 · 2025-08-16T16:30:27Z

Because of the substantial differences both in content and purpose of the above changes, I have moved the development of this to a new pull request at #3618

docs: started work on a type reference

e271b21

joelberkeley reviewed Aug 5, 2025

View reviewed changes