I would like to represent IPv4 addresses in dhall, so I can manage my host configurations.
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.
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.
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,
My questions are:
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).This is what I've tried:
{-# 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
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
(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?
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:
For example, if this were a question about native support for dates/times, I'd give the same answer (for the same reasons).
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
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
).
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 }
... and that confirms that the extra 1-field record wrapping the type is what is interfering with decoding.
The reason for this unexpected type is because of how you derived the Interpret
instance for IP
here:
instance Interpret IP where
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))))
The Generic
representation of the IP
type is a record with one (anonymous) field, where that one field contains the 4-tuple of Word8
s. 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).
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 :)
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)
The main changes I made were:
GeneralizedNewtypeDeriving
language extensionGeneric
instance for IP
Show
instance for IP
(for debugging)... and then that works:
*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))
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With