Создавайте простые функции с зависимыми типами - PullRequest
Новая
       9

Создавайте простые функции с зависимыми типами

0 голосов
/ 15 февраля 2019

Я учусь на официальной документации .Я попытался изменить первый пример: 

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)
-}

Я понятия не имею, почему мои функции не возвращают типы.Они похожи на коды Идриса, но не работают.

1 Ответ

0 голосов
/ 15 февраля 2019

Ваш тип функций не является полным.Вы можете проверить это с помощью :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
...