Refinement Type trong Haskell
Haskell
18
White

checkraiser viết ngày 06/07/2018

Refinement Type trong Haskell

Giới thiệu về Refinement Type

Mình đang tìm hiểu về Refinement Type và áp dụng nó vào Haskell.

Có 1 ví dụ ở đây

Đại loại là, bạn cần khai báo 1 kiểu dữ liệu khoảng (i, j), với điều kiện là i >= 0, j >= 0, i < j

data Interval  = I
  { _from :: Int
  , _to   :: Int
  } deriving (Show)

có nghĩa là, nếu chương trình của bạn có khai báo:

x1 = I 10 5
x2 = I -1 3

thì nó sẽ báo lỗi là KHÔNG ĐÚNG kiểu dữ liệu bạn cần lưu ! (Mặc dù compiler nói là đúng rồi -_!)

Quá cool, đúng không.

Vậy làm thế nào ??

Đầu tiên là cài đặt LiquidHasskellđây

sau đó test với ví dụ trong bài viết ở trên:

{-@ type Nat = { v: Int | v >= 0} @-}
data Interval  = I
  { _from :: Int
  , _to   :: Int
  } deriving (Show)
{-@ data Interval = I
       { _from :: Nat
       , _to   :: {v: Nat | _from < v }
    }
@-}
x1 = I 10 5
x2 = I (-1) 3

Chương trình này là well-typed trong Haskell. Vấn đề là nó sai bét !

Có 2 refinement mà mình khai ở trên:

  • Khai báo kiểu Nat là tập hợp các số tự nhiên, tức là các số nguyên có giá trị lớn hơn hoặc bằng 0.
  • Khai báo _from, _to cùng thuộc kiểu số tự nhiên với _to > _from.

Viết 1 bash script để kiểm tra xem

#!/bin/bash
stack exec -- liquid -i api $1

Nó sẽ báo lỗi:


Type Mismatch

 175 | x2 = I (-1) 3
               ^^

   Inferred type
     VV : {v : Int | v == (-?a)
                     && v == ?b}

   not a subtype of Required type
     VV : {VV : Int | VV >= 0}

   In Context
     ?b : {?b : Int | ?b == (-?a)}

     ?a : {?a : Int | ?a == (1 : int)}

Đúng như mình mong đợi, x1x2 là 2 giá trị sai.

Cool hơn, nếu mình lấy x1x2 từ bàn phím:

testItv = do
  x1 <- P.getLine
  let x = P.read x1
  y1 <- P.getLine
  let y = P.read y1
  print $ I x y

Chương trình này cũng hoàn toàn well-typed !, nhưng rất tiếc, nó sai bét .

Dùng liquid để kiểm tra, nó ném ra lỗi:

Error: Liquid Type Mismatch

 180 |   print $ I x y
                 ^^^^^

   Inferred type
     VV : {v : Int | v == y}

   not a subtype of Required type
     VV : {VV : Int | VV >= 0
                      && x < VV}

   In Context
     x : Int

     y : Int

Quá đúng những gì mình mong đợi !

Tích hợp vs VSCode

Mình dùng snippet sau để thêm các check mình cần:

"LiquidHaskell pragmas": {
        "prefix": "liquid",
        "body": [
            "{-@ LIQUID ${1|\"--short-names\",\"--exact-data-con\",\"--no-adt\",\"--prune-unsorted\",\"--higherorder\",\"--no-termination\"|} @-}"
        ],
        "description": "Add liquid pragma"
    }   

Nó có thể check cả totaltermination của chương trình ! (MÌnh chưa test)


{-@ LIQUID "--short-names" @-}
{-@ LIQUID "--exact-data-con" @-}
{-@ LIQUID "--no-adt" @-}
{-@ LIQUID "--prune-unsorted" @-}
{-@ LIQUID "--higherorder" @-}
{-@ LIQUID "--no-termination" @-}

Lưu ý khi dùng Custom PreludeByteString

Nếu bạn muốn dùng 1 custom prelude như Protolude, và có cả ByteString thì dưới đây là 1 cách khai báo:

{-# LANGUAGE NoImplicitPrelude #-}
import qualified Data.ByteString.Lazy as BL
import qualified Data.ByteString.Lazy.Char8 as C
import qualified Prelude as P
import Protolude

checkraiser 06-07-2018

Bình luận


White
{{ comment.user.name }}
Bỏ hay Hay
{{comment.like_count}}
Male avatar
{{ comment_error }}
Hủy
   

Hiển thị thử

Chỉnh sửa

White

checkraiser

17 bài viết.
20 người follow
Kipalog
{{userFollowed ? 'Following' : 'Follow'}}
Cùng một tác giả
White
6 1
Tôi dự sẽ viết 1 loạt series về việc thiết kế 1 ứng dụng Rails như thế nào để nó có thể giúp bạn ăn ngon ngủ yên trong hằng năm trời: Khi mà việc t...
checkraiser viết 3 năm trước
6 1
White
5 10
Cũng ngót nghét đi làm hơn 6 năm rồi, mình chỉ thấy một điều khá "ngược đời": Các ông chủ , những người trả tiền cho bạn lại có tư duy lập trình ké...
checkraiser viết 1 năm trước
5 10
White
3 3
This post is a sample chapter from my (Link) How to render a ReactJS component isomorphically ? The trick is in defaultProps and componentDidM...
checkraiser viết hơn 3 năm trước
3 3
Bài viết liên quan
White
14 6
Người ta nói "nullable values" là cái "billion dollar mistake". Kể từ ALGOL, chúng ta không thể dùng nullable values/references như một value bình ...
Justin Le viết hơn 3 năm trước
14 6
White
3 0
Đọc hiểu được type signature là một trong các yếu tố quyết định chuyện bạn có học Haskell được hay không. Đa số chúng ta khi mới tìm hiểu thường g...
Huy Trần viết 9 tháng trước
3 0
White
4 2
Trong (Link), tôi có đề cập đến cách bắt đầu với Haskell bằng cách cài đặt Haskell Platform. Sau một thời gian mày mò không biết bao nhiêu thời gia...
viethnguyen viết hơn 3 năm trước
4 2
{{like_count}}

kipalog

{{ comment_count }}

bình luận

{{liked ? "Đã kipalog" : "Kipalog"}}


White
{{userFollowed ? 'Following' : 'Follow'}}
17 bài viết.
20 người follow

 Đầu mục bài viết

Vẫn còn nữa! x

Kipalog vẫn còn rất nhiều bài viết hay và chủ đề thú vị chờ bạn khám phá!