git.iko.soy/Idris-dev
on master help sign in
Add FAQ answer on implicitly bound names
6592938Edwin Brady
docs/faq/faq.rst+53
compare with master
unifiedsplit
@@ -103,6 +103,59 @@ the difference between:
103 Idris> \n, m => n + (S m)
103 Idris> \n, m => n + (S m)
104 \n => \m => plus n (S m) : Nat -> Nat -> Nat
104 \n => \m => plus n (S m) : Nat -> Nat -> Nat
105
105
106+
107+Why can't I use a function with no arguments in a type?
108+=======================================================
109+
110+If you use a name in a type which begins with a lower case letter, and which is
111+not applied to any arguments, then Idris will treat it as an implicitly
112+bound argument. For example:
113+
114+.. code-block:: idris
115+
116+ append : Vect n ty -> Vect m ty -> Vect (n + m) ty
117+
118+Here, ``n``, ``m``, and ``ty`` are implicitly bound. This rule applies even
119+if there are functions defined elsewhere with any of these names. For example,
120+you may also have:
121+
122+.. code-block:: idris
123+
124+ ty : Type
125+ ty = String
126+
127+Even in this case, ``ty`` is still considered implicitly bound in the definition
128+of ``append``, rather than making the type of ``append`` equivalent to...
129+
130+.. code-block:: idris
131+
132+ append : Vect n String -> Vect m String -> Vect (n + m) String
133+
134+...which is probably not what was intended! The reason for this rule is so
135+that it is clear just from looking at the type of ``append``, and no other
136+context, what the implicitly bound names are.
137+
138+If you want to use an unapplied name in a type, you have two options. You
139+can either explicitly qualify it, for example, if ``ty`` is defined in the
140+namespace ``Main`` you can do the following:
141+
142+.. code-block:: idris
143+
144+ append : Vect n Main.ty -> Vect m Main.ty -> Vect (n + m) Main.ty
145+
146+Alternatively, you can use a name which does not begin with a lower case
147+letter, which will never be implicitly bound:
148+
149+.. code-block:: idris
150+
151+ Ty : Type
152+ Ty = String
153+
154+ append : Vect n Ty -> Vect m Ty -> Vect (n + m) Ty
155+
156+As a convention, if a name is intended to be used as a type synonym, it is
157+best for it to begin with a capital letter to avoid this restriction.
158+
106I have an obviously terminating program, but Idris says it possibly isn't total. Why is that?
159I have an obviously terminating program, but Idris says it possibly isn't total. Why is that?
107=============================================================================================
160=============================================================================================
108
161