我读这个，我觉得这样的：

措施 -为了使Haskell函数出现在细化类型中，我们需要将其提升到细化类型级别。

还有其他一些文件声称需要采取措施在合同中使用这种功能。但是我尝试了这个：

{-@ len :: List a -> Nat @-}
len :: List a -> Int
len Nil           = 0
len (x `Cons` xs) = 1 + len xs

{-@ mymap :: (a -> b) -> xs : List a -> { ys : List b | len xs == len ys } @-}
mymap :: (a -> b) -> List a -> List b
mymap _ Nil           = Nil
mymap f (x `Cons` …

我在Haskell中有一个响应Json输入的服务器.问题是,有些情况下服务器会因部分功能而崩溃,但Liquid Haskell表示这是安全的.

这是一个最小的工作示例:

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DeriveGeneric #-}

module Main where

import qualified Web.Scotty as Scot
import GHC.Generics (Generic)
import qualified Data.Aeson as Json
import Data.Text.Internal.Lazy (Text)

main :: IO ()
main =
  Scot.scotty 3000 $
    Scot.get "/:queryJson" $ do
      rawRequest <- Scot.param "queryJson"
      case Json.decode rawRequest of
        Nothing -> Scot.text "Could not decode input."
        Just input -> Scot.text $ makeOutput (dim1 input)

{-@ type Dim = { x : Int | x >= 0 && x …

我正在尝试解决LiquidHaskell 教程中的一些练习。所以，我这样写：

data List a = Nil | Cons a (List a) deriving (Show)                                                                                  
infixr 5 `Cons`

{-@ len :: List a -> Nat @-}
len :: List a -> Int
len Nil           = 0
len (x `Cons` xs) = 1 + len xs

{-@ mymap :: (a -> b) -> xs : List a -> { ys : List b | len xs == len ys } @-}
mymap :: (a -> b) -> List a -> List …

问题

我一直很兴奋使用LiquidHaskell,但是,我不知道我需要在多大程度上修改我原来的Haskell代码以满足LiquidHaskell的要求.

下面是一个简单的例子,说明Liquid的规范如何适用于String类型,但不适用于Text类型.

对于String类型,它运行良好

例

我定义了一个Liquid类型,我们说元组的值不能相同:

{-@ type NoRouteToHimself = {v:(_, _) | (fst v) /= (snd v)} @-}

然后,对于String类型规范,它运行良好,如下所示:

{-@ strOk :: NoRouteToHimself @-}
strOk :: (String, String)
strOk = ("AA", "AB")

LiquidHaskel输出>> 结果:安全

{-@ strBad :: NoRouteToHimself @-}
strBad :: (String, String)
strBad = ("AA", "AA")

LiquidHaskel输出>> 结果:UNSAFE

到目前为止,我们为Text类型定义了相同的函数.

对于Text类型,它出错了

例

{-# LANGUAGE OverloadedStrings #-}
import qualified Data.Text as Tx

{-@ foo :: NoRouteToHimself @-}
foo :: (Tx.Text, Tx.Text)
foo …

我遵循的是Liquid Haskell的官方教程，偶然发现了其中的“ bug”。

本教程中包含以下代码，而Liquid Haskell应该检查它是否安全。

{-@ type TRUE  = {v:Bool | v    } @-}
{-@ type FALSE = {v:Bool | not v} @-}

{-@ (==>) :: p:Bool -> q:Bool -> {v:Bool | v <=> (p ==> q)} @-}
False ==> False = True
False ==> True  = True
True  ==> True  = True
True  ==> False = False

{-@ measure f :: Int -> Int @-}

{-@ congruence :: (Int -> Int) …

我正在尝试在NixOS上使用liquidhaskell.我可以安装包(liquidhaskell-0.8.2.3),虽然不是cabal集成,因为它需要cabal 1.18-1.25,但我有cabal 2.0.1.0.

我已经安装了liquidhaskell软件包作为ghc-with-packages设置的一部分:

[~:0]$ readlink $( type -p liquid )
/nix/store/pdbzl0p6k1klmajx969b6vvwyw9w0s6b-ghc-8.2.2-with-packages/bin/liquid

在许多其他方面,包文本也安装在这个集合中:

[proclib:1]$ ls -ld /nix/store/pdbzl0p6k1klmajx969b6vvwyw9w0s6b-ghc-8.2.2-with-packages/lib/ghc-8.2.2/text-1.2.2.2/
dr-xr-xr-x 3 root root 68 Jan  1  1970 /nix/store/pdbzl0p6k1klmajx969b6vvwyw9w0s6b-ghc-8.2.2-with-packages/lib/ghc-8.2.2/text-1.2.2.2/

但是液体看不出来:

[proclib:1]$ liquid ~/bin/h/nix.hs 
LiquidHaskell Version 0.8.2.3
Copyright 2013-18 Regents of the University of California. All Rights Reserved.

liquid: Main: Could not find module ‘Data.Text’
Perhaps you meant Data.Set (from containers-0.5.10.2)
Use -v to see a list of the files searched for.

以上不是cabal包的一部分(试图从等式中消除阴谋).

我尝试过使用nix-shell来完成这项工作,但无论是nix-shell还是液体都会破坏语言编译指示:

[~:0]$ nix-shell -p myHaskellEnv --run liquid ~/bin/h/nix.hs 
/nix/store/q1cwqhb6v8yx8vy4s5p6sxrq8s0bnqmy-nix.hs: line 5: …

我最近一直在玩LiquidHaskell和Idris,我得到了一个非常具体的问题,我无法在任何地方找到明确的答案.

伊德里斯是一种依赖类型的语言,在很大程度上是很好的.但是我读到类型检查期间的某些类型术语可以从编译时"泄漏"到运行时,即使是强硬的Idris也会尽力消除这些术语(这甚至是一个特殊功能......).然而,这种消除并不完美,有时确实会发生.如果,为什么以及何时发生这种情况并未立即从代码中清除,有时会对运行时性能产生影响.

我见过人们更喜欢Haskells的类型系统,因为它不会发生在那里.完成类型检查后,即可完成.类型被"丢弃"并且在运行时不使用.

LiquidHaskell的故事是什么？与传统的Haskell相比,它增强了类型系统的功能.LiquidHaskell是否也为某些类型的"星座"注入运行时位,或者(我怀疑)只是在Haskell上添加了另一层"更好"的类型,它们不会影响任何形状或形式的运行时.

意思是,如果删除特殊的LiquidHaskell类型注释并使用标准GHC编译它,生成的代码是否始终相同？换句话说:LiquidHaskell扩展只是编译时间吗？

如果是的话,这似乎是两个世界中最好的,或者LiquidHaskell在类型系统中不像Idris那样具有表现力,因此没有运行时条款管理？

以下代码尝试将Unsigned索引处的 Clash 类型族细化4为Digit：

import Clash.Prelude

{-@ type Digit = {v : Unsigned 4 | v <= 9 } @-}
type Digit = Unsigned 4

{-@ foo :: Digit -> Digit @-}
foo = id @Digit

这会导致以下错误消息：

The Liquid type
.
    (Clash.Sized.Internal.Unsigned.Unsigned {4}) -> (Clash.Sized.Internal.Unsigned.Unsigned {4})
.
is inconsistent with the Haskell type
.
    Clash.Sized.Internal.Unsigned.Unsigned 4
-> Clash.Sized.Internal.Unsigned.Unsigned 4
.
defined at src/HelloClash.hs:11:1-3
.
Specifically, the Liquid component
.
    {4}
.
is inconsistent with the …

是否有带注释的变体或Haskell Prelude可用于轻松移植调用诸如head或的函数的现有程序length？

我在使用LiquidHaskell证明以下法律时遇到了麻烦:

它被称为DeMorgan定律(之一),并简单地指出,or对两个值的否定必须and与每个值的否定相同.它已经被证明了很长时间,并且是LiquidHaskell 教程中的一个例子.我正在学习本教程,但未能通过以下代码:

-- Test.hs
module Main where

main :: IO ()
main = return ()

(==>) :: Bool -> Bool -> Bool
False ==> False = True
False ==> True  = True
True  ==> True  = True
True  ==> False = False

(<=>)  :: Bool -> Bool -> Bool
False <=> False = True
False <=> True  = False
True  <=> True  = True
True  <=> False = False

{-@ type TRUE  = {v:Bool …