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”从文字(例如 Char、String 或 Integer)转换为所需的任何类型(如上述来源之一的注释中所述:[...] '-5' 脱糖为 'negate (fromInteger 5)')，一般来说 Idris1 支持任意两种类型的隐式转换。 (http://docs.idris-lang.org/en/latest/tutorial/miscellany.html#implicit-conversions)

就 Idris2 而言，有一些 pragmas (%charLit fromChar, %stringLit fromString, %integerLit fromInteger) 提示编译器使用某些从文字到任何其他类型的转换函数.