使用依赖类型创建简单函数

Question

我正在学习the official documentation。我试图修改第一个例子：

isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

这是我的尝试：

compute_type : Integer  -> Type
compute_type 1 = Nat
compute_type 2 = String

--foo : (x : Integer) -> compute_type x
-- foo 1     = Z
-- foo 2 = ?one --unwords ["A", "B", "C"]

错误：

{-
first_class_type.idr:7:13:
  |
7 | foo 1     = Z
  |             ^
When checking right hand side of foo with expected type
        compute_type 1

Type mismatch between
        Nat (Type of 0)
and
        compute_type 1 (Expected type)
-}

ct2 : String -> Type
ct2 "Integer" = Integer
ct2 "String"  = String
foo2 : (s : String) -> ct2 s
-- foo2 "Integer" = 42

错误：

{-
   |
28 | foo2 "Integer" = 42
   |                  ~~
When checking right hand side of foo2 with expected type
        ct2 "Integer"

ct2 "Integer" is not a numeric type
-}

ct3: Bool -> Bool -> Type
ct3 True True = Nat
ct3 False False = String

foo3: (a: Bool) -> (b: Bool) -> (ct3 a b)
-- foo3 True True = Z
-- foo3 False False = "Stringggg"

错误：

{-
first_class_type.idr:44:18:
   |
44 | foo3 True True = Z
   |                  ^
When checking right hand side of foo3 with expected typ
        ct3 True True

Type mismatch between
        Nat (Type of 0)
and
        ct3 True True (Expected type)

Holes: Main.foo3, Main.foo2
-}

ct4: (b: String) -> Type
ct4 "Integer" = Integer
ct4 "String"  = String
foo4: (s: String) -> ct4 s -> Integer
-- foo4 "Integer" x = x
-- foo4 "String" ss = 987

错误：

{-
   |
67 | foo4 "Integer" x = x
   |                    ^
When checking right hand side of foo4 with expected type
        Integer

Type mismatch between
        ct4 "Integer" (Type of x)
and
        Integer (Expected type)
-}

我不知道为什么我的函数不返回类型。它们看起来与Idris代码类似，但它们不起作用。

Answer 1

你的类型函数不是完整的。您可以使用:total foo进行检查或指定该函数应为total：

%default total
-- or
total foo : Integer -> Type

只有总函数才能在类型检查器中得到解析，否则它可能会或可能不会永远运行。如果你想坚持Integer和String，为了使你的功能完全，你可以添加一个默认情况：

compute_type : Integer  -> Type
compute_type 1 = Nat
compute_type _ = String

foo : compute_type 1
foo = Z