idris - Prelude 如何允许 Nat 使用数字文字？

Question

在 Idris ch 的类型驱动开发中。 4，他们说

The Prelude also defines functions and notation to allow Nat to be used like any other numeric type, so rather than writing S (S (S (S Z))), you can simply write 4.

和 Fin 类似.它是如何实现这一目标的？我看过 the source但我想不通。

Answer 1

从哪里链接通知fromIntegerNat :

||| Convert an Integer to a Nat, mapping negative numbers to 0
fromIntegerNat : Integer -> Nat
fromIntegerNat 0 = Z
fromIntegerNat n =
  if (n > 0) then
    S (fromIntegerNat (assert_smaller n (n - 1)))
  else
    Z

和 fromInteger在 Nat 的 Num 实现中:

Num Nat where
  (+) = plus
  (*) = mult

  fromInteger = fromIntegerNat

并转换整数 Nat

||| Casts negative `Integers` to 0.
Cast Integer Nat where
  cast = fromInteger

在 Idris1 的情况下，它将尝试通过那些“fromFunctions”(如上述来源之一的评论中所述: [...] '-5' desugars to 'negate (fromInteger 5)')将文字(例如 Char、String 或 Integer)转换为所需的任何类型一般来说，Idris1 支持任何两种类型的隐式转换。 ( http://docs.idris-lang.org/en/latest/tutorial/miscellany.html#implicit-conversions )

在Idris2的情况下，有一些 pragmas ( %charLit fromChar , %stringLit fromString , %integerLit fromInteger ) 提示编译器使用一些从文字到任何其他类型的强制转换函数。