我如何代表dhall中的元组?

use*_*536 10 haskell dhall

我想在dhall中表示IPv4地址,因此我可以管理我的主机配置.

默认情况下,它保持为Text; 但这显然不能令人满意,因为它允许任何旧文本漏掉.我想将这些值保持为8位值的4元组.

我不认为Dhall本身可以允许这种情况 - 我能看到的最接近的是{a:Natural,b:Natural}等的记录,但这在语法上是笨重的,并且仍然允许在0-255之外的八位字节值.

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

我的问题是:

  1. 我是否认为直接在Dhall中这样做是不可能或不成比例的?
  2. 要在Haskell中定义此类型,我是否要定义一个实例Interpret; 如果是这样,我如何定义一个将在4部分的整数列表中读取的实例,同时为错误构造的错误长度列表(错误长度的列表,非整数列表或非列表)或out -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
Run Code Online (Sandbox Code Playgroud)

但我正在努力寻找一种方法来表达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
Run Code Online (Sandbox Code Playgroud)

(我更愿意表达一个IP,比如说,[1,2,3,4];但是在错误消息和文档之后pair似乎表明编号的记录是要走的路).

有没有办法实现我追求的目标?

Gab*_*lez 5

对于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
Run Code Online (Sandbox Code Playgroud)

错误消息现在显示“类型差异”,它说明两种类型之间的差异。在这种情况下,差异已经暗示了这个问题,那就是有一个额外的记录封装了该类型。它认为应该只有一个_1在最外层的四个领域和_1/ _2/ _3/ _4我们的预期很可能嵌套在该领域内的字段(这就是为什么它认为,_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
Run Code Online (Sandbox Code Playgroud)

关键部分是消息的底部,其中指出:

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 }
Run Code Online (Sandbox Code Playgroud)

...并确认包装该类型的额外1字段记录正在干扰解码。

这种意外类型的原因是由于您如何Interpret在IP此处派生实例:

instance Interpret IP where
Run Code Online (Sandbox Code Playgroud)

当你省略了Interpret实例执行它倒在使用Generic实例IP是不一样的Generic实例(Word8, Word8, Word8, Word8)。您可以通过要求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))))
Run Code Online (Sandbox Code Playgroud)

类型的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)
Run Code Online (Sandbox Code Playgroud)

...尽管那并不能真正解决您的问题:)

因此,如果您希望IP类型具有与Interpret实例相同的实例,(Word8, Word8, Word8, Word8)则实际上您不想使用GHC Generics来为派生Interpret实例IP。您真正想要的是使用,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)
Run Code Online (Sandbox Code Playgroud)

我进行的主要更改是:

  • 添加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)
Run Code Online (Sandbox Code Playgroud)

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

{-# 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))
Run Code Online (Sandbox Code Playgroud)