жирная стрела в Идрисе

Что ж, в Haskell сигнатуры и значения типов находятся в разных пространствах имен, поэтому что-то, определенное в одном, не рискует конфликтовать с чем-то в другом. В Idris типы и значения занимают одно и то же пространство имен, поэтому вы не видите, например. data Foo = Foo как в Haskell, а скорее data Foo = MkFoo - тип называется Foo, а конструктор называется MkFoo, так как уже есть значение (тип Foo), привязанное к имени Foo, например data Pair = MkPair http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#tuples Так что, вероятно, это к лучшему, что он не пытался использовать стрелку, используемую для построения типа функций, со стрелкой, используемой для лямбда-выражений - это довольно разные вещи. Вы можете комбинировать их, например, с the (Int -> Int) (\x => x).

Я думаю, это потому, что они по-разному интерпретируют символ ->. Из Википедии:

A => B означает, что если A верно, то B также верно; если A ложно, то ничего не говорится о B

что кажется правильным для выражений case, и

-> может означать то же, что и =>, или может иметь значение для функций, указанных ниже.

который

f: X -> Y означает, что функция f отображает набор X в набор Y

Итак, я предполагаю, что Идрис использует -> только для узкого второго значения, то есть для сопоставления одного типа с другим в сигнатурах типов, тогда как Haskell использует более широкую интерпретацию, где это означает то же, что и =>.