Skip to content

Instantly share code, notes, and snippets.

@guibou
Created December 31, 2022 16:50
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save guibou/32762816ace8e9c8509ace5570e73c96 to your computer and use it in GitHub Desktop.
Save guibou/32762816ace8e9c8509ace5570e73c96 to your computer and use it in GitHub Desktop.
Iso 8601 duration parsing at type level
ghci> duration @"P1Y1W"
Duration {years = 1, months = 0, days = 0, weeks = 1, hours = 0, minutes = 0, seconds = 0}
ghci> duration @"P1Y1WT10H5M"
Duration {years = 1, months = 0, days = 0, weeks = 1, hours = 10, minutes = 5, seconds = 0}
ghci> duration @"P1Y1WT10H5M120S"
Duration {years = 1, months = 0, days = 0, weeks = 1, hours = 10, minutes = 5, seconds = 120}
ghci> duration @"P10H5M120S"
<interactive>:119:1: error:
• Cannot parse duration. Expecting 'T', got: 10H5M120S
• In the expression: duration @"P10H5M120S"
In an equation for ‘it’: it = duration @"P10H5M120S"
ghci> duration @"PT10H5M120S"
Duration {years = 0, months = 0, days = 0, weeks = 0, hours = 10, minutes = 5, seconds = 120}
ghci> duration @"PT10H5M120STrailing?"
<interactive>:121:1: error:
• Cannot parse duration at: Trailing?
• In the expression: duration @"PT10H5M120STrailing?"
In an equation for ‘it’: it = duration @"PT10H5M120STrailing?"
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{- |
This modules parses ISO 8601 duration at type level.
It proposes the 'Duration' type as well as 'duration' function, which returns
a 'Duration' from a type level string.
It behaves exactly as you would implement a partial `IsString` instance, but
instead of simple implementation leading to a runtime crash with explicit
error, it fails at compile time with an awful error and the implementation is
ugly.
-}
module Iso8601Duration (Duration(..), duration) where
import GHC.OverloadedLabels (IsLabel(..))
import GHC.TypeLits
import Data.Type.Bool (If)
import Data.Type.Equality
import Data.Data (Proxy(..))
-- * Number parsing
type family ParseNumber s where
ParseNumber s = ParseNumberInner (UnconsSymbol s) Nothing
type family ParseNumberInner t n where
ParseNumberInner Nothing s = '(s, "")
ParseNumberInner (Just '(c, cs)) n = If (IsDigit c) (ParseNumberInner (UnconsSymbol cs) (Just (FromMaybe 0 n * 10 + FromJust (ToDigit c)))) '(n, ConsSymbol c cs)
-- * Number followed by letter
type family ParseNumberFollowedByLetter s l where
ParseNumberFollowedByLetter s l = ParseNumberFollowedByLetterInternal (ParseNumber s) l
type family ParseNumberFollowedByLetterInternal s l where
ParseNumberFollowedByLetterInternal '(Nothing, s) _ = Nothing
ParseNumberFollowedByLetterInternal '(Just number, s) l = ParseNumberFollowedByLetterInternal2 number (UnconsSymbol s) l
type family ParseNumberFollowedByLetterInternal2 n s l where
ParseNumberFollowedByLetterInternal2 n Nothing l = Nothing
ParseNumberFollowedByLetterInternal2 n (Just '( c, cs)) l = If (CmpChar c l == EQ) (Just '(n, cs)) Nothing
--
-- * Digits
type family IsDigit c where
IsDigit c = IsJust (ToDigit c)
type family ToDigit c where
ToDigit '0' = Just 0
ToDigit '1' = Just 1
ToDigit '2' = Just 2
ToDigit '3' = Just 3
ToDigit '4' = Just 4
ToDigit '5' = Just 5
ToDigit '6' = Just 6
ToDigit '7' = Just 7
ToDigit '8' = Just 9
ToDigit '9' = Just 9
ToDigit _ = Nothing
-- * Maybe utils
type family FromMaybe v m where
FromMaybe v Nothing = v
FromMaybe _ (Just v) = v
type family IsJust m where
IsJust Nothing = 'False
IsJust (Just _) = 'True
type family FromJust m where
FromJust (Just v) = v
-- * Parsing
type family ParseTimeField s where
ParseTimeField s = ParseFieldsInternal '[ 'H', 'M', 'S' ] s
type family ParseDateField s where
ParseDateField s = ParseFieldsInternal '[ 'Y', 'M', 'D', 'W' ] s
type family ParseFieldsInternal fields s where
ParseFieldsInternal '[] s = '( '[], s)
ParseFieldsInternal (l ': ls) s = ParseFieldsInternal2 l (ParseNumberFollowedByLetter s l) ls s
type family ParseFieldsInternal2 l currentL ls s where
ParseFieldsInternal2 currentL Nothing ls s = ConcatListFirstField '(0, currentL) (ParseFieldsInternal ls s)
ParseFieldsInternal2 currentL (Just '(n, s')) ls s = ConcatListFirstField '(n, currentL) (ParseFieldsInternal ls s')
type family ParseAllFields s where
ParseAllFields s = ParseAllFields' (UnconsSymbol s)
type family ParseAllFields' s where
ParseAllFields' (Just '( 'P', xs ) ) = ParseAllFields'' (ParseDateField xs)
ParseAllFields' _ = TypeError (Text "Duration must start by P.")
type family ParseAllFields'' s where
ParseAllFields'' '( dateFields, s) = ConcatList dateFields (ParseAllFields''' (UnconsSymbol s))
type family ParseAllFields''' s where
ParseAllFields''' Nothing = '[ '(0, 'H'), '(0, 'M'), '(0, 'S')]
ParseAllFields''' (Just '( 'T', xs ) ) = ParseAllFields'''' (ParseTimeField xs)
ParseAllFields''' (Just '( x, xs ) ) = TypeError (Text "Cannot parse duration. Expecting 'T', got: " :<>: Text (ConsSymbol x xs))
type family ParseAllFields'''' s where
ParseAllFields'''' '( timeFields, "") = timeFields
ParseAllFields'''' '( timeFields, s) = TypeError (Text "Cannot parse duration at: " :<>: Text s)
-- * List utils
type family ConcatListFirstField x y where
ConcatListFirstField x '(xs, v) = '(x ': xs, v)
type family ConcatList a b where
ConcatList '[] b = b
ConcatList (a ': as) b = a ': ConcatList as b
-- * Durations
data Duration = Duration {
years :: Int,
months :: Int,
days :: Int,
weeks :: Int,
hours :: Int,
minutes :: Int,
seconds :: Int
}
deriving (Show)
nat :: forall (n :: Nat). KnownNat n => Proxy n -> Int
nat _ = fromInteger (natVal (Proxy @n))
duration :: forall durationText years months days weeks hours minutes seconds. ('[ '(years, 'Y'), '(months, 'M'), '(days, 'D'), '(weeks, 'W'), '(hours, 'H'),
'(minutes, 'M'), '(seconds, 'S')] ~ ParseAllFields durationText,
KnownNat years,
KnownNat months,
KnownNat days,
KnownNat weeks,
KnownNat hours,
KnownNat minutes,
KnownNat seconds
) => Duration
duration = Duration {
years = nat (Proxy @years),
months = nat (Proxy @months),
days = nat (Proxy @days),
weeks = nat (Proxy @weeks),
hours = nat (Proxy @hours),
minutes = nat (Proxy @minutes),
seconds = nat (Proxy @seconds)
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment