Как мне представить кортеж в dhall? - PullRequest
0 голосов
/ 07 февраля 2019

Я хотел бы представлять адреса IPv4 в dhall, чтобы я мог управлять своими конфигурациями хоста.

По умолчанию это текстовое поле;но это явно неудовлетворительно, поскольку позволяет любому старому тексту проскальзывать.Я хотел бы сохранить эти значения как 4-х кортеж из 8-битных значений.

Я не думаю, что Dhall может разрешить это изначально - самое близкое, что я вижу, это запись {a: Natural,b: Natural} и т. д., но это синтаксически неуклюже и по-прежнему допускает значения октетов за пределами 0-255.

Предполагая, что я не могу достичь этого непосредственно в Dhall, возможно, я смогу определить тип в Haskellкоторые могут автоматически читать значения из списков Naturals из Dhall, состоящих из 4 длин,

Мои вопросы:

  1. Правильно ли я считаю, что делать это непосредственно в Dhall невозможно или непропорциональноhard?
  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, похоже, указывают на то, что нумерованная запись - это то, что нужно).

Есть ли способ достичь того, чего я добиваюсь?

1 Ответ

0 голосов
/ 12 февраля 2019

Для 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

В сообщении об ошибке теперь отображается «разность типов», которая объясняеткак два типа отличаются.В этом случае diff уже намекает на проблему, заключающуюся в том, что существует одна дополнительная запись, заключающая в себе тип.Он думает, что на внешнем уровне должно быть только одно поле _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

Ключевая часть является нижней частью сообщения, которое гласит:

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

Когда вы опускаете *При реализации экземпляра 1039 * он использует экземпляр Generic для IP, который NOT совпадает с экземпляром 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))))

Представление Generic типа IP представляет собой запись с одним (анонимным) полем, где этоодно поле содержит 4 кортежа Word8 с.Представление Generic типа (Word8, Word8, Word8, Word8) представляет собой запись из 4 полей (каждое из которых содержит Word8).Вы, вероятно, ожидали последнее поведение (самая внешняя запись из 4 полей), а не прежнее поведение (самая внешняя запись из 1 поля).

Фактически, мы можем получить ожидаемое поведение, декодировав прямо в (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)

... хотя это действительно не решит вашу проблему:)

Так что если вы хотите, чтобы тип 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)

Основные изменения, которые я сделал:

  • Добавление расширения GeneralizedNewtypeDeriving
  • Удаление *Экземпляр 1080 * для 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))
...