我如何在dhall中表示一个元组? [英] How do I represent a tuple in dhall?

查看:96
本文介绍了我如何在dhall中表示一个元组?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

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

I would like to represent IPv4 addresses in dhall, so I can manage my host configurations.

默认情况下,它以文本形式保存;但这显然不尽人意,因为它允许任何旧文本漏掉.我想将这些值保留为8位值的4元组.

By default, this is held as Text; but that's clearly unsatisfactory as it allows any old text to slip through. I would like to keep these values as a 4-tuple of 8-bit values.

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

I don't think that Dhall can allow this natively - the nearest I can see is a record of { a : Natural, b : Natural }, etc., but that's syntactically clunky and still allows for octet values outside of 0-255.

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

Assuming that I can't achieve this directly in Dhall, perhaps I can define a type in Haskell that can automatically read values that are 4-length lists of Naturals from Dhall,

我的问题是:

  1. 我是否认为在Dhall中直接执行此操作是不可能或不成比例地困难?
  2. 要在Haskell中定义此类型,我要定义Interpret的实例吗?如果是这样,那么我如何定义一个实例,该实例将读取一个由四部分组成的整数列表,同时为错误构造(错误长度的列表,非整数或非列表的列表)或有用的错误消息提供有用的错误消息边界值(不介于0和255之间的整数).
  1. Am I right to think that doing this directly in Dhall is impossible or disproportionately hard?
  2. To define this type in Haskell, do I define an instance of Interpret; and if so, how do I define an instance that will read in a 4-part list of Integers, while giving useful error messages for mis-constructed (lists of the wrong length, lists of non-integers or non-lists) or out-of-bounds values (integers that aren't between 0 & 255 inclusive).

这是我尝试过的:

{-# 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中读取的值:

But I'm struggling to find a way to express a value in dhall that can be read in:

λ> 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的文档,似乎暗示编号记录是要走的路).

(I'd much rather express an IP as, say, [1,2,3,4]; but following the error messages and the doc for pair seemed to suggest that the numbered record is the way to go).

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

Is there a way to achieve what I'm after?

推荐答案

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

For IP addresses, I'd recommend representing them as Dhall strings in the absence of language support for the type. There are two main reasons I suggest this:

  • 如果该语言原本就支持IP地址,那么它将为您的用户提供最流畅的迁移路径(只需删除引号即可)
  • 通常,总会存在语言无法完美建模以使无效状态无法表示的数据类型.如果数据类型非常适合Dhall的类型系统,则可以利用它,但是如果不能,请不要强行使用它,否则会使您和您的用户感到沮丧. Dhall不一定是完美的.比YAML好.

例如,如果这是关于日期/时间的本机支持的问题,我会给出相同的答案(出于相同的原因).

For example, if this were a question about native support for dates/times, I'd give the same answer (for the same reasons).

也就是说,我仍然会帮助您调试遇到的问题.我所做的第一件事是尝试使用更新版本的dhall程序包重现此问题,因为该错误信息得到了改进:

That said, I'll still help debug the issue you ran into. The first thing I did was to attempt to reproduce the issue using a newer version of the dhall package since that has improved error messages:

*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

错误消息现在显示"type diff",它说明两种类型的不同之处.在这种情况下,差异已经暗示了这个问题,那就是有一个额外的记录封装了该类型.它认为最外层应该只有一个_1字段,而我们期望的四个_1/_2/_3/_4字段可能嵌套在该字段内(这就是为什么它认为_1字段存储记录而不是Natural).

The error message now shows a "type diff" which explains how the two types differ. In this case the diff already hints at the problem, which is that there is one extra record wrapping the type. It thinks there should only be a single _1 field at the outermost level and the four _1/_2/_3/_4 fields we expected are probably nested inside that field (which is why it thinks that the _1 field stores a record instead of a Natural).

但是,我们可以通过将内容包装在detailed函数中(与命令行上的--explain标志等效)来请求更多详细信息:

However, we can ask for more detail by wrapping things in the detailed function which is equivalent to the --explain flag on the command line:

*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

关键部分是消息的底部,内容为:

The key part is the bottom of the message, which says:

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字段记录是否在干扰解码.

... and that confirms that the extra 1-field record wrapping the type is what is interfering with decoding.

这种意外类型的原因是因为您如何在此处派生IPInterpret实例:

The reason for this unexpected type is because of how you derived the Interpret instance for IP here:

instance Interpret IP where

当您省略Interpret实例实现时,它会使用IP实例作为IP实例,而 NOT (Word8, Word8, Word8, Word8)实例的Generic实例相同.您可以通过要求GHC打印出两种类型的通用表示来确认这一点:

When you omit the Interpret instance implementation it falls back on using the Generic instance for IP which is NOT the same as the Generic instance for (Word8, Word8, Word8, Word8). You can confirm this by asking GHC to print out the generic representation of the two types:

*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))))

IP类型的Generic表示形式是具有一个(匿名)字段的记录,其中一个字段包含4个元组的Word8 s. (Word8, Word8, Word8, Word8)类型的Generic表示形式是4个字段的记录(每个字段包含一个Word8).您可能希望后者的行为(最外层记录为4个字段)而不是前者的行为(最外层记录为1个字段).

The Generic representation of the IP type is a record with one (anonymous) field, where that one field contains the 4-tuple of Word8s. The Generic representation of the (Word8, Word8, Word8, Word8) type is a record of 4 fields (each of which contains a Word8). You probably expected the latter behavior (an outermost record of 4 fields) rather than the former behavior (an outermost record of 1 field).

实际上,我们可以通过直接解码为(Word8, Word8, Word8, Word8)类型来获得您期望的行为:

In fact, we can get the behavior you expected by decoding straight into a (Word8, Word8, Word8, Word8) type:

*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)

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

... although that doesn't really solve your problem :)

因此,如果您希望IP类型具有与(Word8, Word8, Word8, Word8)相同的Interpret实例,那么您实际上不希望使用GHC Generics派生IPInterpret实例.您真正想要的是使用GeneralizedNewtypeDeriving,以便newtype使用与基础类型完全相同的实例.您可以使用以下代码来做到这一点:

So if you want the IP type to have the same Interpret instance as (Word8, Word8, Word8, Word8) then you actually do not want to use GHC Generics to derive the Interpret instance for IP. What you actually want is to use GeneralizedNewtypeDeriving so that the newtype uses the exact same instance as the underlying type. You can do that with the following code:

{-# 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语言扩展
  • 删除IPGeneric实例
  • IP添加Show实例(用于调试)
  • Adding the GeneralizedNewtypeDeriving language extension
  • Removing the Generic instance for IP
  • Adding a Show instance for IP (for debugging)

...然后可行:

*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)

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

You can also do this without any orphan instances, like this:

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

这篇关于我如何在dhall中表示一个元组?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!

查看全文
登录 关闭
扫码关注1秒登录
发送“验证码”获取 | 15天全站免登陆