Как указать функцию, работающую с непустой структурой данных, с помощью LiquidHaskell?

Question

Я пытаюсь выполнить первое упражнение в тематическом исследовании LiquidHaskell о Lazy Queues

module Main where

main :: IO ()
main = putStrLn "hello"

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

{-@ die :: {v:String | false} -> a @-}
die x = error x

{-@ measure realSize @-}
realSize      :: [a] -> Int
realSize []     = 0
realSize (_:xs) = 1 + realSize xs

{-@ data SList a = SL {
       size  :: Nat 
     , elems :: {v:[a] | realSize v = size}
     }
  @-}
data SList a = SL { size :: Int, elems :: [a]}

{-@ type NEList a = {v:SList a | 0 < size v} @-}

{-@ hd           :: NEList a -> a @-}
hd (SL _ (x:_))  = x 
hd _             = die "empty SList"

okList = SL 1 ["cat"]
okHd   = hd okList

okHd терпит неудачу:

 app/Main.hs:30:13-18: Error: Liquid Type Mismatch
   Inferred type
     VV : {VV : (SList [Char]) | VV == Main.okList}

   not a subtype of Required type
     VV : {VV : (SList [Char]) | 0 < size VV}

   In Context
     VV : {VV : (SList [Char]) | VV == Main.okList}
     Main.okList
        : (SList [Char])

Судя по сообщению об ошибке, я почти уверен, что не предоставляю достаточно информации LH, чтобы он "знал", что okList не пусто, но я не могу понять, как это исправить.

Я попытался сказать это явно с постусловием (?):

{-@ okList :: NEList a @-}
okList = SL 1 ["cat"]

Но это не работает:

 app/Main.hs:29:5: Error: Specified Type Does Not Refine Haskell Type for Main.okList
 Haskell: Main.SList [GHC.Types.Char]
 Liquid : forall a. Main.SList a

Answer 1

Ваш изысканный тип okList не ограничивает тип. Он ограничил размер, но потерял тип из String в a,

+ Изменить

{-@ okList :: NEList a @-}
okList = SL 1 ["cat"]

в

{-@ okList :: NEList String @-}
okList = SL 1 ["cat"]

И это будет работать.

---

Я должен признать, что я не очень хорошо знаю liquidhaskell, поэтому все, что ниже, может быть только моим диким предположением:

Основная причина, по которой вы должны это сделать, это то, что вы определяете okList отдельно с конструктором по умолчанию SL, Изысканный тип SList только обещает, что size v = realSize (elems v)размер списка проверяется при вызове конструктора, сравнивается с числовым литералом и затем отбрасывается, а не сохраняется на уровне типа (жидкости). Поэтому, когда вы кормите okList в hdединственная информация, доступная для рассуждения size v = realSize (elems v) (из уточненного типа данных) и size v >= 0 (size определяется как Nat), hd не будет знать, если это положительно.

В hd okList, liquidhaskell может быть не в состоянии оценить выражение и тем самым заменить okList с Sl 1 ["cat"] и получить информацию о размере, так что он может только сделать суждение, зависит от уточненного типа okList это сделало вывод (в этом случае SList String). Одним из доказательств является hd $ SL 1 ["cat"] будет работать без уточненного типа.