haskell - 我如何在 dhall 中表示一个元组？

Question

我想在 dhall 中表示 IPv4 地址，这样我就可以管理我的主机配置。

默认情况下，这被保存为文本；但这显然不能令人满意，因为它允许任何旧文本通过。我想将这些值保留为 8 位值的 4 元组。

我不认为 Dhall 可以本机允许这一点 - 我能看到的最接近的是 { a : Natural, b : Natural } 等的记录，但这在语法上很笨拙，并且仍然允许 0-255 之外的八位字节值。

假设我不能直接在 Dhall 中实现这一点，也许我可以在 Haskell 中定义一个类型，它可以自动从 Dhall 读取 4 长度的 Naturals 列表的值，

我的问题是：

我是否认为直接在 Dhall 中执行此操作是不可能的或异常困难的？
要在 Haskell 中定义这种类型，我需要定义一个Interpret;的实例吗？如果是这样，我如何定义一个实例，该实例将在 4 部分整数列表中读取，同时为错误构造（错误长度的列表、非整数列表或非列表）或输出提供有用的错误消息-of-bounds 值（不介于 0 和 255 之间的整数）。

这是我尝试过的：

{-# LANGUAGE DeriveGeneric   #-}
{-# LANGUAGE RecordWildCards #-}

import Control.Applicative  ( empty, pure )
import Dhall  ( Generic, Interpret( autoWith ), Type( Type, extract, expected ) )
import Dhall.Core  ( Expr( Natural, NaturalLit ) )
import Data.Word  ( Word8 )

newtype IP = IP (Word8, Word8, Word8, Word8)
  deriving Generic

word8 :: Type Word8
word8 = Type {..}
  where
    extract (NaturalLit n) | n >= 0 && n <= 255 = pure (fromIntegral n)
    extract  _             = empty

    expected = Natural

instance Interpret Word8 where
  autoWith _ = word8

instance (Interpret a,Interpret b,Interpret c,Interpret d) => Interpret (a,b,c,d)

instance Interpret IP where

但我正在努力寻找一种方法来表达可以读入的 dhall 值：

λ> input auto "{ _1 = 1, _2 = 2, _3 = 3, _4 = 5 } : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural}" :: IO IP
*** Exception: 
Error: Expression doesn't match annotation

{ _1 = 1, _2 = 2, _3 = 3, _4 = 5 } : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural}

(input):1:1

（我更愿意将 IP 表示为 [1,2,3,4]；但遵循错误消息和文档pair似乎表明编号记录是要走的路）。

有没有办法实现我所追求的？

score 5 · Accepted Answer

对于 IP 地址，我建议在没有对该类型的语言支持的情况下将它们表示为 Dhall 字符串。我建议这样做的主要原因有两个：

如果该语言本身确实支持 IP 地址，那么这将为您的用户提供最顺畅的迁移路径（只需去掉引号）
通常，总会存在语言无法完美建模以使无效状态无法表示的数据类型。如果数据类型很适合 Dhall 的类型系统，那么就利用它，但如果不适合，则不要强迫它，否则你会挫败你自己和你的用户。Dhall 不一定要完美。比 YAML 更好。

例如，如果这是关于日期/时间的本地支持的问题，我会给出相同的答案（出于相同的原因）。

也就是说，我仍然会帮助调试您遇到的问题。我做的第一件事是尝试使用较新版本的dhall软件包重现该问题，因为它改进了错误消息：

*Main Dhall> input auto "{ _1 = 1, _2 = 2, _3 = 3, _4 = 5 } : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural}" :: IO IP
*** Exception: 
Error: Expression doesn't match annotation

{ + _2 : …
, + _3 : …
, + _4 : …
,   _1 : - { … : … }
         + Natural
}

{ _1 = 1, _2 = 2, _3 = 3, _4 = 5 } : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural} : { _1 : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural } }
(input):1:1

错误消息现在显示“类型差异”，它解释了这两种类型的不同之处。在这种情况下，差异已经暗示了问题所在，即有一个额外的记录包装了该类型。它认为最外层应该只有一个字段，_1而我们预期的四个///_1字段可能嵌套在该字段内（这就是为什么它认为该字段存储一条记录而不是一条记录）。_2_3_4_1Natural

但是，我们可以通过在函数中包装一些东西来询问更多细节，detailed这相当于--explain命令行上的标志：

*Main Dhall> detailed (input auto "{ _1 = 1, _2 = 2, _3 = 3, _4 = 5 } : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural}" :: IO IP)
*** Exception: 
Error: Expression doesn't match annotation

{ + _2 : …
, + _3 : …
, + _4 : …
,   _1 : - { … : … }
         + Natural
}

Explanation: You can annotate an expression with its type or kind using the     
❰:❱ symbol, like this:                                                          


    ┌───────┐                                                                   
    │ x : t │  ❰x❱ is an expression and ❰t❱ is the annotated type or kind of ❰x❱
    └───────┘                                                                   

The type checker verifies that the expression's type or kind matches the        
provided annotation                                                             

For example, all of the following are valid annotations that the type checker   
accepts:                                                                        


    ┌─────────────┐                                                             
    │ 1 : Natural │  ❰1❱ is an expression that has type ❰Natural❱, so the type  
    └─────────────┘  checker accepts the annotation                             


    ┌───────────────────────┐                                                   
    │ Natural/even 2 : Bool │  ❰Natural/even 2❱ has type ❰Bool❱, so the type    
    └───────────────────────┘  checker accepts the annotation                   


    ┌────────────────────┐                                                      
    │ List : Type → Type │  ❰List❱ is an expression that has kind ❰Type → Type❱,
    └────────────────────┘  so the type checker accepts the annotation          


    ┌──────────────────┐                                                        
    │ List Text : Type │  ❰List Text❱ is an expression that has kind ❰Type❱, so 
    └──────────────────┘  the type checker accepts the annotation               


However, the following annotations are not valid and the type checker will
reject them:                                                                    


    ┌──────────┐                                                                
    │ 1 : Text │  The type checker rejects this because ❰1❱ does not have type  
    └──────────┘  ❰Text❱                                                        


    ┌─────────────┐                                                             
    │ List : Type │  ❰List❱ does not have kind ❰Type❱                           
    └─────────────┘                                                             


Some common reasons why you might get this error:                               

● The Haskell Dhall interpreter implicitly inserts a top-level annotation       
  matching the expected type                                                    

  For example, if you run the following Haskell code:                           


    ┌───────────────────────────────┐                                           
    │ >>> input auto "1" :: IO Text │                                         
    └───────────────────────────────┘                                           


  ... then the interpreter will actually type check the following annotated     
  expression:                                                                   


    ┌──────────┐                                                                
    │ 1 : Text │                                                                
    └──────────┘                                                                


  ... and then type-checking will fail                                          

────────────────────────────────────────────────────────────────────────────────

You or the interpreter annotated this expression:                               

↳   { _1 = 1, _2 = 2, _3 = 3, _4 = 5 }
  : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural }

... with this type or kind:                                                     

↳ { _1 : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural } }

... but the inferred type or kind of the expression is actually:                

↳ { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural }

────────────────────────────────────────────────────────────────────────────────

{ _1 = 1, _2 = 2, _3 = 3, _4 = 5 } : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural} : { _1 : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural } }
(input):1:1

关键部分是消息的底部，它说：

You or the interpreter annotated this expression:                               

↳   { _1 = 1, _2 = 2, _3 = 3, _4 = 5 }
  : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural }

... with this type or kind:                                                     

↳ { _1 : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural } }

... but the inferred type or kind of the expression is actually:                

↳ { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural }

...这证实了包装类型的额外 1 字段记录是干扰解码的原因。

这种意外类型的原因是因为您在此处派生Interpret实例的方式IP：

instance Interpret IP where

当您省略实例Interpret实现时，它会使用与. 您可以通过要求 GHC 打印出这两种类型的通用表示来确认这一点：GenericIPGeneric(Word8, Word8, Word8, Word8)

*Main Dhall> import GHC.Generics
*Main Dhall GHC.Generics> :kind! Rep IP
Rep IP :: * -> *
= D1
    ('MetaData "IP" "Main" "main" 'True)
    (C1
       ('MetaCons "IP" 'PrefixI 'False)
       (S1
          ('MetaSel
             'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
          (Rec0 (Word8, Word8, Word8, Word8))))
*Main Dhall GHC.Generics> :kind! Rep (Word8, Word8, Word8, Word8)
Rep (Word8, Word8, Word8, Word8) :: * -> *
= D1
    ('MetaData "(,,,)" "GHC.Tuple" "ghc-prim" 'False)
    (C1
       ('MetaCons "(,,,)" 'PrefixI 'False)
       ((S1
           ('MetaSel
              'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
           (Rec0 Word8)
         :*: S1
               ('MetaSel
                  'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
               (Rec0 Word8))
        :*: (S1
               ('MetaSel
                  'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
               (Rec0 Word8)
             :*: S1
                   ('MetaSel
                      'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
                   (Rec0 Word8))))

该类型的Generic表示IP是具有一个（匿名）字段的记录，其中一个字段包含Word8s 的 4 元组。类型的Generic表示(Word8, Word8, Word8, Word8)是 4 个字段的记录（每个字段都包含一个Word8）。您可能期望后一种行为（4 个字段的最外层记录）而不是前一种行为（1 个字段的最外层记录）。

事实上，我们可以通过直接解码成一个(Word8, Word8, Word8, Word8)类型来得到你期望的行为：

*Main Dhall GHC.Generics> detailed (input auto "{ _1 = 1, _2 = 2, _3 = 3, _4 = 5 } : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural}" :: IO (Word8, Word8, Word8, Word8))
(1,2,3,5)

...虽然这并不能真正解决您的问题:)

因此，如果您希望该IP类型具有与该类型相同的Interpret实例，那么(Word8, Word8, Word8, Word8)您实际上并不想使用 GHCGenerics派生. 您真正想要的是使用与基础类型完全相同的实例。您可以使用以下代码执行此操作：InterpretIPGeneralizedNewtypeDerivingnewtype

{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RecordWildCards            #-}

import Control.Applicative  ( empty, pure )
import Dhall  ( Generic, Interpret( autoWith ), Type( Type, extract, expected ) )
import Dhall.Core  ( Expr( Natural, NaturalLit ) )
import Data.Word  ( Word8 )

newtype IP = IP (Word8, Word8, Word8, Word8)
  deriving (Interpret, Show)

word8 :: Type Word8
word8 = Type {..}
  where
    extract (NaturalLit n) | n >= 0 && n <= 255 = pure (fromIntegral n)
    extract  _             = empty

    expected = Natural

instance Interpret Word8 where
  autoWith _ = word8

instance (Interpret a,Interpret b,Interpret c,Interpret d) => Interpret (a,b,c,d)

我所做的主要更改是：

添加GeneralizedNewtypeDeriving语言扩展
删除Generic实例IP
为（用于调试）添加Show实例IP

...然后就可以了：

*Main Dhall GHC.Generics> input auto "{ _1 = 1, _2 = 2, _3 = 3, _4 = 5 } : { _1 : Natural, _2 : Natural, _3 : Natural, _4 : Natural}" :: IO IP
IP (1,2,3,5)

您也可以在没有任何孤立实例的情况下执行此操作，如下所示：

{-# LANGUAGE RecordWildCards #-}

import Control.Applicative (empty, pure)
import Data.Coerce (coerce)
import Dhall (Interpret(..), Type(..), genericAuto)
import Dhall.Core (Expr(..))
import Data.Word (Word8)

newtype MyWord8 = MyWord8 Word8

word8 :: Type MyWord8
word8 = Type {..}
  where
    extract (NaturalLit n)
        | n >= 0 && n <= 255 = pure (MyWord8 (fromIntegral n))
    extract _ =
        empty

    expected = Natural

instance Interpret MyWord8 where
  autoWith _ = word8

newtype IP = IP (Word8, Word8, Word8, Word8)
    deriving (Show)

instance Interpret IP where
    autoWith _ = coerce (genericAuto :: Type (MyWord8, MyWord8, MyWord8, MyWord8))

haskell - 我如何在 dhall 中表示一个元组？

1 回答 1

Related

Reference