diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Version 0.1
+
+* Consider this a preview release: The API is likely to stay stable, but
+  extensive testing, formalization and tooling is due.
+
diff --git a/LICENSE.txt b/LICENSE.txt
new file mode 100644
--- /dev/null
+++ b/LICENSE.txt
@@ -0,0 +1,30 @@
+Copyright (c) 2018, Renzo Carbonara
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Renzo Carbonara nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,14 @@
+# di-df1
+
+Write logs in the [df1](https://hackage.haskell.org/package/df1) using
+[di-core](https://hackage.haskell.org/package/di-core) or
+[di-monad](https://hackage.haskell.org/package/di-monad).
+
+Consider this a preview release: The API is likely to stay stable, but extensive
+testing, formalization and tooling is due.
+
+[![Build Status](https://travis-ci.org/k0001/di.svg?branch=master)](https://travis-ci.org/k0001/di)
+
+See the [BSD3 LICENSE](https://github.com/k0001/di/blob/master/di-df1/LICENSE.txt)
+file to learn about the legal terms and conditions for this library.
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,4 @@
+#! /usr/bin/env nix-shell
+#! nix-shell ./shell.nix -i runghc
+import Distribution.Simple
+main = defaultMain
diff --git a/di-df1.cabal b/di-df1.cabal
new file mode 100644
--- /dev/null
+++ b/di-df1.cabal
@@ -0,0 +1,46 @@
+name: di-df1
+version: 1.0
+author: Renzo Carbonara
+maintainer: renλren.zone
+copyright: Renzo Carbonara 2018
+license: BSD3
+license-file: LICENSE.txt
+extra-source-files: README.md CHANGELOG.md
+category: Logging
+build-type: Simple
+cabal-version: >=1.18
+synopsis: Write logs in the df1 format using the di logging framework
+description: Write logs in the df1 format using the di logging framework.
+homepage: https://github.com/k0001/di
+bug-reports: https://github.com/k0001/di/issues
+
+library
+  hs-source-dirs: lib
+  default-language: Haskell2010
+  exposed-modules: Di.Df1 Di.Df1.Monad
+  build-depends:
+    base >=4.9 && <5.0,
+    df1,
+    di-core,
+    di-monad,
+    di-handle,
+    stm
+  ghcjs-options: -Wall -O3
+  ghc-options: -Wall -O2
+
+test-suite test
+  default-language: Haskell2010
+  type: exitcode-stdio-1.0
+  hs-source-dirs: test
+  main-is: Main.hs
+  build-depends:
+    base,
+    bytestring,
+    df1,
+    di-core,
+    di-df1,
+    QuickCheck,
+    text,
+    time,
+    tasty,
+    tasty-quickcheck
diff --git a/lib/Di/Df1.hs b/lib/Di/Df1.hs
new file mode 100644
--- /dev/null
+++ b/lib/Di/Df1.hs
@@ -0,0 +1,355 @@
+{-# LANGUAGE RankNTypes #-}
+
+-- | This module extends extends the /di logging ecosystem/ with support for the
+-- [df1](https://hackage.haskell.org/package/df1) hierarchical structured
+-- logging format.
+--
+-- Particularly, it exports 'df1' for rendering /df1/-formatted logs, an
+-- extension to the "Di.Core" API with vocabulary specific to /df1/, and
+-- functions like 'fromDiLog' or 'fromDf1Log' to convert back and forth between
+-- /di/ and /df1/ types.
+--
+-- The "Di.Df1.Monad" module belonging to this same package exports an extension
+-- to the "Di.Monad" API, rather than to "Di.Core".
+--
+-- Consider this a preview release: The API is likely to stay stable, but
+-- extensive testing, formalization and tooling is due.
+module Di.Df1
+ ( -- * Hierarchy
+   push
+   -- * Metadata
+ , attr
+   -- * Messages
+ , debug
+ , info
+ , notice
+ , warning
+ , error
+ , alert
+ , critical
+ , emergency
+   -- ** Non 'MonadIO' variants
+ , debug'
+ , info'
+ , notice'
+ , warning'
+ , error'
+ , alert'
+ , critical'
+ , emergency'
+
+   -- * "Di.Handle" support
+ , df1
+   -- * Conversion
+ , fromDiLog
+ , fromDf1Log
+ ) where
+
+import Control.Concurrent.STM (STM)
+import Control.Monad.IO.Class (MonadIO)
+import Prelude hiding (error)
+import Unsafe.Coerce (unsafeCoerce)
+
+import qualified Di.Core as Di (Di, Log(Log), log, log', push)
+import qualified Di.Handle as Di (LineRenderer(LineRendererUtf8))
+import qualified Df1
+
+--------------------------------------------------------------------------------
+
+-- | Push a new 'Df1.Segment' to the 'Di.Di'
+push
+  :: Df1.Segment
+  -> Di.Di level Df1.Path msg
+  -> Di.Di level Df1.Path msg   -- ^
+push s = Di.push (Df1.Push s)
+{-# INLINE push #-}
+
+-- | Push a new attribute 'Df1.Key' and 'Df1.Value' to the 'Di.Di'.
+attr
+  :: Df1.Key
+  -> Df1.Value
+  -> Di.Di level Df1.Path msg
+  -> Di.Di level Df1.Path msg   -- ^
+attr k v = Di.push (Df1.Attr k v)
+{-# INLINE attr #-}
+
+--------------------------------------------------------------------------------
+-- MonadIO variants.
+
+-- | Log a message stating that the system is unusable.
+--
+-- @
+-- 'emergency' == 'Di.log' 'Df1.Emergency'
+-- @
+emergency
+  :: MonadIO m
+  => Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+emergency di = Di.log di Df1.Emergency
+{-# INLINE emergency #-}
+
+-- | Log a condition that should be corrected immediately, such as a corrupted
+-- database.
+--
+-- @
+-- 'alert' == 'Di.log' 'Df1.Alert'
+-- @
+alert
+  :: MonadIO m
+  => Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+alert di = Di.log di Df1.Alert
+{-# INLINE alert #-}
+
+-- | Log a critical condition that could result in system failure, such as a
+-- disk running out of space.
+--
+-- @
+-- 'critical' == 'Di.log' 'Df1.Critical'
+-- @
+critical
+  :: MonadIO m
+  => Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+critical di = Di.log di Df1.Critical
+{-# INLINE critical #-}
+
+-- | Log an error condition, such as an unhandled exception.
+--
+-- @
+-- 'error' == 'Di.log' 'Df1.Error'
+-- @
+error
+  :: MonadIO m
+  => Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+error di = Di.log di Df1.Error
+{-# INLINE error #-}
+
+-- | Log a warning condition, such as an exception being gracefully handled or
+-- some missing configuration setting being assigned a default value.
+--
+-- @
+-- 'warning' == 'Di.log' 'Df1.Warning'
+-- @
+warning
+  :: MonadIO m
+  => Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+warning di = Di.log di Df1.Warning
+{-# INLINE warning #-}
+
+-- | Log a condition that is not an error, but should possibly be handled
+-- specially.
+--
+-- @
+-- 'notice' == 'Di.log' 'Df1.Notice'
+-- @
+notice
+  :: MonadIO m
+  => Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+notice di = Di.log di Df1.Notice
+{-# INLINE notice #-}
+
+-- | Log an informational message.
+--
+-- @
+-- 'info' == 'Di.log' 'Df1.Info'
+-- @
+info
+  :: MonadIO m
+  => Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+info di = Di.log di Df1.Info
+{-# INLINE info #-}
+
+-- | Log a message intended to be useful only when deliberately debugging a
+-- program.
+--
+-- @
+-- 'debug' == 'Di.log' 'Df1.Debug'
+-- @
+debug
+  :: MonadIO m
+  => Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+debug di = Di.log di Df1.Debug
+{-# INLINE debug #-}
+
+--------------------------------------------------------------------------------
+-- STM variants
+
+-- | Log a message stating that the system is unusable.
+--
+-- @
+-- 'emergency'' == 'Di.log'' 'Df1.Emergency'
+-- @
+emergency'
+  :: MonadIO m
+  => (forall x. STM x -> m x)
+  -> Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+emergency' natSTM di = Di.log' natSTM di Df1.Emergency
+{-# INLINE emergency' #-}
+
+-- | Log a condition that should be corrected immediately, such as a corrupted
+-- database.
+--
+-- @
+-- 'alert'' == 'Di.log'' 'Df1.Alert'
+-- @
+alert'
+  :: MonadIO m
+  => (forall x. STM x -> m x)
+  -> Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+alert' natSTM di = Di.log' natSTM di Df1.Alert
+{-# INLINE alert' #-}
+
+-- | Log a critical condition that could result in system failure, such as a
+-- disk running out of space.
+--
+-- @
+-- 'critical'' == 'Di.log'' 'Df1.Critical'
+-- @
+critical'
+  :: MonadIO m
+  => (forall x. STM x -> m x)
+  -> Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+critical' natSTM di = Di.log' natSTM di Df1.Critical
+{-# INLINE critical' #-}
+
+-- | Log an error condition, such as an unhandled exception.
+--
+-- @
+-- 'error'' == 'Di.log'' 'Df1.Error'
+-- @
+error'
+  :: MonadIO m
+  => (forall x. STM x -> m x)
+  -> Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+error' natSTM di = Di.log' natSTM di Df1.Error
+{-# INLINE error' #-}
+
+-- | Log a warning condition, such as an exception being gracefully handled or
+-- some missing configuration setting being assigned a default value.
+--
+-- @
+-- 'warning'' == 'Di.log'' 'Df1.Warning'
+-- @
+warning'
+  :: MonadIO m
+  => (forall x. STM x -> m x)
+  -> Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+warning' natSTM di = Di.log' natSTM di Df1.Warning
+{-# INLINE warning' #-}
+
+-- | Log a condition that is not an error, but should possibly be handled
+-- specially.
+--
+-- @
+-- 'notice'' == 'Di.log'' 'Df1.Notice'
+-- @
+notice'
+  :: MonadIO m
+  => (forall x. STM x -> m x)
+  -> Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+notice' natSTM di = Di.log' natSTM di Df1.Notice
+{-# INLINE notice' #-}
+
+-- | Log an informational message.
+--
+-- @
+-- 'info'' == 'Di.log'' 'Df1.Info'
+-- @
+info'
+  :: MonadIO m
+  => (forall x. STM x -> m x)
+  -> Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+info' natSTM di = Di.log' natSTM di Df1.Info
+{-# INLINE info' #-}
+
+-- | Log a message intended to be useful only when deliberately debugging a
+-- program.
+--
+-- @
+-- 'debug'' == 'Di.log'' 'Df1.Debug'
+-- @
+debug'
+  :: MonadIO m
+  => (forall x. STM x -> m x)
+  -> Di.Di Df1.Level path Df1.Message
+  -> Df1.Message
+  -> m ()
+debug' natSTM di = Di.log' natSTM di Df1.Debug
+{-# INLINE debug' #-}
+
+--------------------------------------------------------------------------------
+
+-- | A 'LineRenderer' to be used with tools like 'Di.Handle.handle' or
+-- 'Di.Handle.stderr' from the "Di.Handle" module.
+df1 :: Di.LineRenderer Df1.Level Df1.Path Df1.Message
+{-# INLINE df1 #-}
+df1 = Di.LineRendererUtf8 (\x ->
+  if x then Df1.renderColor . fromDiLog
+       else Df1.render . fromDiLog)
+
+--------------------------------------------------------------------------------
+
+-- | Convert a 'Df1.Log' from "Df1" to a 'Di.Log' from "Di.Core".
+--
+-- @
+-- 'fromDiLog' . 'fromDf1Log'  ==  'id'
+-- @
+--
+-- @
+-- 'fromDf1Log' . 'fromDiLog'  ==  'id'
+-- @
+fromDiLog :: Di.Log Df1.Level Df1.Path Df1.Message -> Df1.Log
+{-# INLINE fromDiLog #-}
+fromDiLog = unsafeCoerce  -- see _fromDiLog
+
+-- | Unused. Just type-checking that the order of arguments didn't change.
+_fromDiLog :: Di.Log Df1.Level Df1.Path Df1.Message -> Df1.Log
+_fromDiLog (Di.Log a b c d) = Df1.Log a b c d
+
+---
+
+-- | Convert a 'Di.Log' from "Di.Core" to a 'Df1.Log' from "Df1".
+--
+-- @
+-- 'fromDiLog' . 'fromDf1Log'  ==  'id'
+-- @
+--
+-- @
+-- 'fromDf1Log' . 'fromDiLog'  ==  'id'
+-- @
+fromDf1Log :: Df1.Log -> Di.Log Df1.Level Df1.Path Df1.Message
+{-# INLINE fromDf1Log #-}
+fromDf1Log = unsafeCoerce  -- see _fromDf1Log
+
+-- | Unused. Just type-checking that the order of arguments didn't change.
+_fromDf1Log :: Df1.Log -> Di.Log Df1.Level Df1.Path Df1.Message
+_fromDf1Log (Df1.Log a b c d) = Di.Log a b c d
+
diff --git a/lib/Di/Df1/Monad.hs b/lib/Di/Df1/Monad.hs
new file mode 100644
--- /dev/null
+++ b/lib/Di/Df1/Monad.hs
@@ -0,0 +1,118 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+-- | This module exports an API compatible with "Di.Monad".
+module Di.Df1.Monad
+ ( -- * Hierarchy
+   push
+   -- * Metadata
+ , attr
+   -- * Messages
+ , debug
+ , info
+ , notice
+ , warning
+ , error
+ , alert
+ , critical
+ , emergency
+ ) where
+
+import Prelude hiding (error)
+
+import qualified Df1
+import qualified Di.Monad as Di (MonadDi, log, push)
+
+--------------------------------------------------------------------------------
+
+-- | Push a new 'Df1.Segment' to the 'Di.MonadDi'.
+push
+  :: Di.MonadDi level Df1.Path msg m
+  => Df1.Segment -> m a -> m a  -- ^
+push s = Di.push (Df1.Push s)
+{-# INLINE push #-}
+
+-- | Push a new attribute 'Df1.Key' and 'Df1.Value' to the 'Di.MonadDi'.
+attr
+  :: Di.MonadDi level Df1.Path msg m
+  => Df1.Key -> Df1.Value -> m a -> m a -- ^
+attr k v = Di.push (Df1.Attr k v)
+{-# INLINE attr #-}
+
+--------------------------------------------------------------------------------
+
+-- | Log a message stating that the system is unusable.
+--
+-- @
+-- 'emergency' == 'Di.log' 'Df1.Emergency'
+-- @
+emergency :: Di.MonadDi Df1.Level path Df1.Message m => Df1.Message -> m () -- ^
+emergency = Di.log Df1.Emergency
+{-# INLINE emergency #-}
+
+-- | Log a condition that should be corrected immediately, such as a corrupted
+-- database.
+--
+-- @
+-- 'alert' == 'Di.log' 'Df1.Alert'
+-- @
+alert :: Di.MonadDi Df1.Level path Df1.Message m => Df1.Message -> m () -- ^
+alert = Di.log Df1.Alert
+{-# INLINE alert #-}
+
+-- | Log a critical condition that could result in system failure, such as a
+-- disk running out of space.
+--
+-- 'critical' == 'Di.log' 'Df1.Critical'
+-- @
+critical :: Di.MonadDi Df1.Level path Df1.Message m => Df1.Message -> m () -- ^
+critical = Di.log Df1.Critical
+{-# INLINE critical #-}
+
+-- | Log an error condition, such as an unhandled exception.
+--
+-- @
+-- 'error' == 'Di.log' 'Df1.Error'
+-- @
+error :: Di.MonadDi Df1.Level path Df1.Message m => Df1.Message -> m () -- ^
+error = Di.log Df1.Error
+{-# INLINE error #-}
+
+-- | Log a warning condition, such as an exception being gracefully handled or
+-- some missing configuration setting being assigned a default value.
+--
+-- @
+-- 'warning' == 'Di.log' 'Df1.Warning'
+-- @
+warning :: Di.MonadDi Df1.Level path Df1.Message m => Df1.Message -> m () -- ^
+warning = Di.log Df1.Warning
+{-# INLINE warning #-}
+
+-- | Log a condition that is not an error, but should possibly be handled
+-- specially.
+--
+-- @
+-- 'notice' == 'Di.log' 'Df1.Notice'
+-- @
+notice :: Di.MonadDi Df1.Level path Df1.Message m => Df1.Message -> m () -- ^
+notice = Di.log Df1.Notice
+{-# INLINE notice #-}
+
+
+-- | Log an informational message.
+--
+-- @
+-- 'info' == 'Di.log' 'Df1.Info'
+-- @
+info :: Di.MonadDi Df1.Level path Df1.Message m => Df1.Message -> m () -- ^
+info = Di.log Df1.Info
+{-# INLINE info #-}
+
+-- | Log a message intended to be useful only when deliberately debugging a
+-- program.
+--
+-- @
+-- 'debug' == 'Di.log' 'Df1.Debug'
+-- @
+debug :: Di.MonadDi Df1.Level path Df1.Message m => Df1.Message -> m () -- ^
+debug = Di.log Df1.Debug
+{-# INLINE debug #-}
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Main where
+
+import Data.String (fromString)
+import qualified Data.Text as T
+import qualified Data.Text.Lazy as TL
+import Data.Time.Clock.System as Time
+import qualified Test.Tasty as Tasty
+import Test.Tasty.QuickCheck ((===))
+import qualified Test.Tasty.QuickCheck as QC
+import qualified Test.Tasty.Runners as Tasty
+
+import qualified Di.Core as Di
+import qualified Di.Df1
+import qualified Df1
+
+--------------------------------------------------------------------------------
+
+main :: IO ()
+main = Tasty.defaultMainWithIngredients
+  [ Tasty.consoleTestReporter
+  , Tasty.listingTests
+  ] tt
+
+tt :: Tasty.TestTree
+tt = Tasty.testGroup "di-df1"
+  [ QC.testProperty "fromDiLog . fromDf1Log == id" $ do
+      QC.forAllShrink QC.arbitrary QC.shrink $ \df1Log -> do
+         df1Log === Di.Df1.fromDiLog (Di.Df1.fromDf1Log df1Log)
+
+  , QC.testProperty "fromDf1Log . fromDiLog == id" $ do
+      QC.forAllShrink QC.arbitrary QC.shrink $ \diLog -> do
+         diLog === Di.Df1.fromDf1Log (Di.Df1.fromDiLog diLog)
+  ]
+
+instance QC.Arbitrary (Di.Log Df1.Level Df1.Path Df1.Message) where
+  arbitrary = Di.Log
+    <$> genSystemTime <*> QC.arbitrary <*> QC.arbitrary <*> QC.arbitrary
+  shrink (Di.Log a b c d) = Di.Log
+    <$> pure a <*> QC.shrink b <*> QC.shrink c <*> QC.shrink d
+
+instance QC.Arbitrary Df1.Log where
+  arbitrary = Df1.Log
+    <$> genSystemTime <*> QC.arbitrary <*> QC.arbitrary <*> QC.arbitrary
+  shrink (Df1.Log a b c d) = Df1.Log
+    <$> pure a <*> QC.shrink b <*> QC.shrink c <*> QC.shrink d
+
+instance QC.Arbitrary Df1.Path where
+  arbitrary = QC.oneof
+    [ Df1.Push <$> QC.arbitrary
+    , Df1.Attr <$> QC.arbitrary <*> QC.arbitrary ]
+  shrink (Df1.Push s) = Df1.Push <$> QC.shrink s
+  shrink (Df1.Attr k v) = Df1.Attr <$> QC.shrink k <*> QC.shrink v
+
+instance QC.Arbitrary Df1.Level where
+  arbitrary = QC.elements [minBound .. minBound]
+
+instance QC.Arbitrary Df1.Segment where
+  arbitrary = fromString <$> QC.arbitrary
+  shrink = map Df1.segment . QC.shrink . Df1.unSegment
+
+instance QC.Arbitrary Df1.Key where
+  arbitrary = fromString <$> QC.arbitrary
+  shrink = map Df1.key . QC.shrink . Df1.unKey
+
+instance QC.Arbitrary Df1.Value where
+  arbitrary = fromString <$> QC.arbitrary
+  shrink = map Df1.value . QC.shrink . Df1.unValue
+
+instance QC.Arbitrary Df1.Message where
+  arbitrary = fromString <$> QC.arbitrary
+  shrink = map Df1.message . QC.shrink . Df1.unMessage
+
+instance QC.Arbitrary T.Text where
+  arbitrary = T.pack <$> QC.arbitrary
+  shrink = map T.pack . QC.shrink . T.unpack
+
+instance QC.Arbitrary TL.Text where
+  arbitrary = TL.pack <$> QC.arbitrary
+  shrink = map TL.pack . QC.shrink . TL.unpack
+
+genSystemTime :: QC.Gen Time.SystemTime
+genSystemTime = do
+  a <- QC.choose (0, 253402300799) -- up to 4 digit years
+  b <- QC.choose (0, 1000000000)
+  pure (Time.MkSystemTime a b)
+