我如何在dhall中代表一个元组？

Question

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

默认情况下，这是作为文本；但这显然不能令人满意，因为它允许任何旧的文本滑过。我想把这些值保持为4元组的8位值.

我不认为Dhall可以允许本机--我能看到的最近的记录是{a:自然科学，b:自然}等等，但这在语法上很笨拙，并且仍然允许在0-255之外的八进制值。

假设我不能在Dhall中直接做到这一点，也许我可以在Haskell中定义一种类型，它可以自动读取来自Dhall的四长自然列表的值，

我的问题是：

1. 我认为直接在Dhall做这件事是不可能的，或者说不成比例的困难，这是正确的吗？
2. 要在Haskell中定义这种类型，我是否定义了Interpret的一个实例；如果是的话，我如何定义一个将读取4部分整数列表的实例，同时为错误构造的(长度错误的列表、非整数或非列表的列表)或界外值(不包含在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文档似乎表明，编号的记录是可行的)。

有办法实现我想要的目标吗？

Answer 1

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

• 如果语言本机支持IP地址，那么它将为用户提供最平滑的迁移路径(只需删除引号)。
• 通常情况下，总是存在语言无法完美建模的数据类型，从而使无效状态无法表示。如果数据类型非常适合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

错误消息现在显示了一个“类型差异”，它解释了这两种类型的区别。在本例中，diff已经提示了问题，即有一个额外的记录包装类型。它认为应该只有一个最外层的_1字段，我们期望的四个_1字段可能嵌套在该字段中(这就是为什么它认为_1字段存储记录而不是Natural)。

但是，我们可以通过将内容包装在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字段记录包装类型是什么干扰了解码。

出现这种意外类型的原因是，您是如何在这里导出IP的IP实例的：

instance Interpret IP where

当省略Interpret实例实现时，它会回到使用IP的Generic实例，即，而不是，与(Word8, Word8, Word8, Word8)的Generic实例相同。您可以通过要求GHC打印出这两种类型的泛型表示来确认这一点：

*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表示是一个带有一个(匿名)字段的记录，其中一个字段包含Word8的4个元组，(Word8, Word8, Word8, Word8)类型的Generic表示是一个由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类型具有与(Word8, Word8, Word8, Word8)相同的Interpret实例，则实际上不希望使用GHC Generics派生IP的Interpret实例。您真正想要的是使用GeneralizedNewtypeDeriving，以便newtype使用与底层类型完全相同的实例。您可以使用以下代码执行此操作：

{-# 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))