创建具有依赖类型的简单函数答案

【问题标题】：Create simple functions with dependent types创建具有依赖类型的简单函数
【发布时间】：2019-02-15 13:50:01
【问题描述】：

我正在向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 代码相似，但它们不起作用。

【问题讨论】：

标签： idris

【解决方案1】：

您的类型功能不是全部。您可以通过:total foo 或指定该函数应该是总的来检查这一点：

%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

【讨论】：