LINUX.ORG.RU
решено Форум — Development  

Тупняк и Idris

 , , ,


0

2

Есть функция:

squareHead : Num a => List a -> a
squareHead (x :: xs) = x * x

по хорошему, оно компилироваться не должно (но компилируется).
В Haskell при пустом списке оно просто выкинет exception, а здесь оно возвращает что-то не совсем понятное:
λΠ> squareHead []
squareHead [] : Integer
λΠ> cast (squareHead []) / 3.0
prim__divFloat (prim__toFloatBigInt (squareHead [])) 3.0 : Double

ЯННП.

★★★★
← c++ bind
А где взять данные о негативых/позитивных высказываниях? →

Coq вообще не даёт возможность для таких махинаций: List.head возвращает option‐тип, а напрямую через паттерн‐матчинг вытащить не получится:

Definition square_head a : nat :=
  match a with
    | cons x _ => x * x
  end.
(* error: Non exhaustive pattern-matching: no clause found for pattern nil *)

awesomelackware ★
()

https://groups.google.com/forum/#!topic/idris-lang/xoHIdqjVIaY

Если по-русски, то Idris по-умолчанию просто не вычисляет функцию для тех веток, что не определены. Если это не подходит, используй --warnpartial (будет предупреждать) или --total (тогда такое не будет компилироваться).

monk ★★★★★
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.
← c++ bind
Development
А где взять данные о негативых/позитивных высказываниях? →