как привести встроенные функции - PullRequest
Новая
       16

как привести встроенные функции

0 голосов
/ 18 апреля 2020

Я делаю первые шаги с Liquid Haskell и думаю о реальном применении. Есть пример с функцией абс. Я хочу использовать встроенную функцию abs, потому что код приложения в любом случае падает на функции из базы. Поэтому я не хочу и не могу скопировать весь базовый модуль. 

{-@ type Nat = {v:Int | 0 <= v } @-}
{-@ myAbs :: Int -> Nat @-}
myAbs :: Int -> Int
myAbs = abs

В последней строке возникла проблема. ЛГ жалуется на абс. Он встроен. Какие варианты у меня есть?

===================== Обновление ================ ======

Следуя дальнейшему руководству, я выяснил, как встроить спецификации для сторонних функций. 

{-@ assume abs :: Num a => a -> {v:a | 0 <= v} @-}

Хотя довольно скоро я наткнулся на слегка усложненную функцию. 

{-@ assume getBounds :: (MArray a e m, Ix i) => a i e -> m (i, i) @-}
-- or
{-@ assume getBounds :: (Monad m, MArray a e m, Ix i) => a i e -> m (i, i) @-}

Выше спецификации указаны отклонения. 

Error: Specified type does not refine Haskell type for `Data.Array.Base.getBounds` (Plugged Init types new)

 45 | {-@ assume getBounds :: (MArray a e m, Ix i) => a i e -> m (i, i) @-}
                              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^


 The Liquid type

     (Data.Array.Base.MArray a e m) -> (GHC.Arr.Ix i) -> a i e -> m (i, i)

 is inconsistent with the Haskell type

     forall (a :: * -> * -> *) e (m :: * -> *) i. (haskell-liquid)
...