Liquid Haskell: ошибка с проверочными комбинаторами и типы, уточненные предикатами - PullRequest
Новая
       35

Liquid Haskell: ошибка с проверочными комбинаторами и типы, уточненные предикатами

0 голосов
/ 28 ноября 2018

В качестве минимального примера проблемы, которую я имею, приведем определение натуральных чисел, функцию удвоения и тип, уточненный предикатом четности: 

data Nat' = Z | S Nat' deriving Show

{-@ reflect double' @-}
double' :: Nat' -> Nat'
double' Z = Z
double' (S x) = (S (S (double' x)))

{-@ type Even' = {v:Nat' | even' v} @-}

{-@ reflect even' @-}
even' :: Nat' -> Bool
even' Z = True
even' (S Z) = False
even' (S (S x)) = even' x

Мне бы хотелосьсначала объявить {-@ double' :: Nat' -> Even' @-}, а затем доказать, что это правда, но у меня сложилось впечатление, что вместо этого я должен сначала написать доказательство, а затем использовать castWithTheorem (который сам для меня работал) как таковой: 

{-@ even_double :: x:Nat' -> {even' (double' x)} @-}
even_double Z =     even' (double' Z) 
              ==.   even' Z  
              ==.   True 
              ***   QED
even_double (S x) =     even' (double' (S x))
                  ==.   even' (S (S (double' x)))
                  ==.   even' (double' x)
                  ?     even_double x
                  ==.   True
                  ***   QED

{-@ double :: Nat' -> Even' @-}
double x = castWithTheorem (even_double x) (double' x)

Однако, это дает довольно неразборчивые ошибки, такие как: 

:1:1-1:1: Error
  elaborate solver elabBE 177 "lq_anf$##7205759403792806976##d3tK" {lq_tmp$x##1556 : (GHC.Types.$126$$126$ (GHC.Prim.TYPE GHC.Types.LiftedRep) (GHC.Prim.TYPE GHC.Types.LiftedRep) bool bool) | [(lq_tmp$x##1556 = GHC.Types.Eq#)]} failed on:
      lq_tmp$x##1556 == GHC.Types.Eq#
  with error
      Cannot unify (GHC.Types.$126$$126$ (GHC.Prim.TYPE GHC.Types.LiftedRep) (GHC.Prim.TYPE GHC.Types.LiftedRep) bool bool) with func(0 , [(GHC.Prim.$126$$35$ @(42) @(43) @(44) @(45));
          (GHC.Types.$126$$126$ @(42) @(43) @(44) @(45))]) in expression: lq_tmp$x##1556 == GHC.Types.Eq# 
  because
Elaborate fails on lq_tmp$x##1556 == GHC.Types.Eq#
  in environment
      GHC.Types.Eq# := func(4 , [(GHC.Prim.$126$$35$ @(0) @(1) @(2) @(3));
                                 (GHC.Types.$126$$126$ @(0) @(1) @(2) @(3))])

      lq_tmp$x##1556 := (GHC.Types.$126$$126$ (GHC.Prim.TYPE GHC.Types.LiftedRep) (GHC.Prim.TYPE GHC.Types.LiftedRep) bool bool)

Что я делаю не так?Судя по моим экспериментам, это вызвано попыткой доказать, что некоторая предикатная функция верна для некоторого аргумента.

1 Ответ

0 голосов
/ 30 ноября 2018

Проблема заключалась в том, что я должен был использовать NewProofCombinators вместо ProofCombinators.Затем замена ==. на === и castWithTheorem (even_double x) (double' x) на (double' x) `withProof` (even_double x) устраняет проблему: http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1543595949_5844.hs

Все найденные мной онлайн-ресурсы используют ProofCombinators, так что, надеюсь, это спасет кого-то от боли.

Источник: https://github.com/ucsd-progsys/liquidhaskell/issues/1378#issuecomment-443262472

...