1 files changed, 232 insertions, 0 deletions
diff --git a/pkgs/profpatsch/xmonad/DhallTypedInput.hs b/pkgs/profpatsch/xmonad/DhallTypedInput.hs
new file mode 100644
index 00000000..18c32b22
--- /dev/null
+++ b/pkgs/profpatsch/xmonad/DhallTypedInput.hs
@@ -0,0 +1,232 @@
+{-# language RecordWildCards, NamedFieldPuns, OverloadedStrings, ScopedTypeVariables, KindSignatures, DataKinds, ScopedTypeVariables, RankNTypes, GADTs, TypeApplications, AllowAmbiguousTypes, LambdaCase #-}
+{- Exports the `inputWithTypeArgs` function, which is able to read dhall files of the normalized form
+
+@
+\(CustomType: Type) ->
+\(AnotherType: Type) ->
+…
+@
+
+and set their actual representation on the Haskell side:
+
+This has various advantages:
+
+- dhall files still type check & normalize with the normal dhall
+  tooling, they are standalone (and the types can be instantiated from
+  dhall as well without any workarounds)
+- It can be used like the default `input` function, no injection of
+  custom symbols in the Normalizer is reqired
+- Brings this style of dhall integration to Haskell, where it was only
+  feasible in nix before, because that is untyped
+
+The dhall types can be instantiated by every Haskell type that has an
+`Interpret` instance. The “name” of the type lambda variable is
+compared on the Haskell side with a type-level string that the user
+provides, to prevent mixups.
+
+TODO:
+- Improve error messages (!)
+- Provide a way to re-use the type mapping on the Haskell side, so
+  that the returned values are not just the normal `Interpret` types,
+  but the mapped ones (with name phantom type)
+-}
+module DhallTypedInput
+( inputWithTypeArgs, TypeArg(..), TypeArgError(..), TypeArgEx(..),  typeArg
+)
+where
+
+import Control.Monad.Trans.State.Strict as State
+import Data.List (foldl')
+import Control.Exception (Exception)
+import qualified Control.Exception
+import qualified Data.Text as Text
+
+import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
+import Data.Proxy (Proxy(Proxy))
+
+import Dhall (Type(..), InvalidType(..), InputSettings(..), EvaluateSettings(..), rootDirectory, startingContext, normalizer, standardVersion, sourceName, defaultEvaluateSettings, Interpret(..), auto)
+import Dhall.TypeCheck (X)
+import Dhall.Core
+import Dhall.Parser (Src(..))
+import qualified Dhall.Import
+import qualified Dhall.Pretty
+import qualified Dhall.TypeCheck
+import qualified Dhall.Parser
+
+import Lens.Family (LensLike', set, view)
+
+import Data.Text.Prettyprint.Doc (Pretty)
+import qualified Data.Text.Prettyprint.Doc               as Pretty
+import qualified Data.Text.Prettyprint.Doc.Render.Text   as Pretty
+import qualified Data.Text.Prettyprint.Doc.Render.String as Pretty
+
+
+-- | Information about a type argument in the dhall input
+--
+-- If the dhall file starts with @\(CustomType : Type) ->@,
+-- that translates to @TypeArg "CustomType" interpretionType@
+-- where @"CustomType"@ is a type-level string describing the
+-- name of the type in the dhall file (as a sanity check) and
+-- @interpretationType@ is any type which implements
+-- 'Dhall.Interpret'.
+--
+-- This is basically a specialized 'Data.Proxy'.
+data TypeArg (sym :: Symbol) t = TypeArg
+
+-- | Existential wrapper of a 'TypeArg', allows to create a list
+-- of heterogenous 'TypeArg's.
+data TypeArgEx
+  where TypeArgEx :: (KnownSymbol sym, Interpret t) => TypeArg sym t -> TypeArgEx
+
+-- | Shortcut for creating a 'TypeArgEx'.
+--
+-- Use with @TypeApplications@:
+--
+-- @
+-- typeArg @"CustomType" @Integer
+-- @
+typeArg :: forall sym t. (KnownSymbol sym, Interpret t) => TypeArgEx
+typeArg = TypeArgEx (TypeArg :: TypeArg sym t)
+
+-- | Possible errors returned when applying a 'TypeArg'
+-- to a 'Dhall.Expr'.
+data TypeArgError
+  = WrongLabel Text.Text
+  -- ^ The name (label) of the type was different,
+  -- the text value is the expected label.
+  | NoLambda
+  -- ^ The 'Dhall.Expr' does not start with 'Dhall.Lam'.
+
+-- | Apply a 'TypeArg' to a 'Dhall.Expr'.
+--
+-- Checks that the dhall file starts with the 'Dhall.Lam'
+-- corresponding to 'TypeArg`, then applies @t@ (dhall type application)
+-- and normalizes, effectively stripping the 'Dhall.Lam'.
+applyTypeArg
+  :: forall sym t. (KnownSymbol sym, Interpret t)
+  => Expr Src X
+  -> TypeArg sym t
+  -> Either TypeArgError (Expr Src X)
+applyTypeArg expr ta@(TypeArg) = case expr of
+  (Lam label (Const Dhall.Core.Type) _)
+    -> let expectedLabel = getLabel ta
+        in if label /= getLabel ta
+           then Left (WrongLabel expectedLabel)
+           else let expr' = (normalize (App expr tExpect))
+                  in Right expr'
+    where
+        Dhall.Type _ tExpect = Dhall.auto :: Dhall.Type t
+  expr -> Left NoLambda
+
+-- | Inflect the type-level string @sym@ to a text value.
+getLabel :: forall sym t. (KnownSymbol sym) => TypeArg sym t -> Text.Text
+getLabel _ = Text.pack $ symbolVal (Proxy :: (Proxy :: Symbol -> *) sym)
+
+instance (KnownSymbol sym) => Show (TypeArg sym t) where
+  show TypeArg =
+    "TypeArg "
+    ++ (symbolVal (Proxy :: (Proxy :: Symbol -> *) sym))
+
+-- | Takes a list of 'TypeArg's and parses the given
+-- dhall string, applying the given 'TypeArg's in order
+-- to the opaque dhall type arguments (see 'TypeArg' for
+-- how these should look).
+--
+-- This is a slightly changed 'Dhall.inputWith'.
+--
+-- Discussion: Any trace of our custom type is removed from
+-- the resulting
+inputWithTypeArgs
+  :: InputSettings
+  -> [TypeArgEx]
+  -> Dhall.Type a
+  -> Text.Text
+  -> IO a
+inputWithTypeArgs settings typeArgs (Dhall.Type {extract, expected}) txt = do
+    expr <- throws (Dhall.Parser.exprFromText (view sourceName settings) txt)
+
+    -- TODO: evaluateSettings not exposed
+    -- let evSettings = view evaluateSettings settings
+    let evSettings :: EvaluateSettings = defaultEvaluateSettings
+
+    -- -vvv copied verbatim from 'Dhall.inputWith' vvv-
+    let transform =
+               set Dhall.Import.standardVersion
+               (view standardVersion evSettings)
+            .  set Dhall.Import.normalizer
+               (view normalizer evSettings)
+            .  set Dhall.Import.startingContext
+               (view startingContext evSettings)
+
+    let status = transform (Dhall.Import.emptyStatus
+                            (view rootDirectory settings))
+
+    expr' <- State.evalStateT (Dhall.Import.loadWith expr) status
+    -- -^^^ copied verbatim ^^^-
+
+    let
+      -- | if there’s a note, run the transformation and rewrap with the note
+      skipNote e f = case e of
+          Note n e -> Note n $ f e
+          e -> f e
+
+    let
+      -- | strip one 'TypeArg'
+      stripTypeArg :: Expr Src X -> TypeArgEx -> Expr Src X
+      stripTypeArg e (TypeArgEx ta) = skipNote e $ \e' -> case e' of
+          (Lam label _ _) ->
+            case applyTypeArg e' ta of
+              Right e'' -> e''
+              -- TODO obvously improve error messages
+              Left (WrongLabel l) ->
+                error $ "Wrong label, should have been `" ++ Text.unpack l ++ "` but was `" ++ Text.unpack label ++ "`"
+              Left NoLambda -> error $ "I expected a lambda of the form λ(" ++ Text.unpack label ++ ": Type) → but got: " ++ show e
+          e' -> error $ show e'
+
+    -- strip all 'TypeArg's
+    let expr'' = foldl' stripTypeArg expr' typeArgs
+
+    -- -vvv copied verbatim as well (expr' -> expr'') vvv-
+    let suffix = prettyToStrictText expected
+    let annot = case expr'' of
+            Note (Src begin end bytes) _ ->
+                Note (Src begin end bytes') (Annot expr'' expected)
+              where
+                bytes' = bytes <> " : " <> suffix
+            _ ->
+                Annot expr'' expected
+
+    _ <- throws (Dhall.TypeCheck.typeWith (view startingContext settings) annot)
+    case extract (Dhall.Core.normalizeWith (Dhall.Core.getReifiedNormalizer (view normalizer settings)) expr'') of
+        Just x  -> return x
+        Nothing -> Control.Exception.throwIO InvalidType
+
+
+-- copied from Dhall.Pretty.Internal
+prettyToStrictText :: Pretty a => a -> Text.Text
+prettyToStrictText = docToStrictText . Pretty.pretty
+
+-- copied from Dhall.Pretty.Internal
+docToStrictText :: Pretty.Doc ann -> Text.Text
+docToStrictText = Pretty.renderStrict . Pretty.layoutPretty options
+  where
+   options = Pretty.LayoutOptions { Pretty.layoutPageWidth = Pretty.Unbounded }
+
+-- copied from somewhere in Dhall
+throws :: Exception e => Either e a -> IO a
+throws (Left  e) = Control.Exception.throwIO e
+throws (Right r) = return r
+
+
+-- TODO: add errors like these
+-- data WrongTypeLabel = WrongTypeLabel deriving (Typeable)
+
+-- _ERROR :: String
+-- _ERROR = "\ESC[1;31mError\ESC[0m"
+
+-- instance Show WrongTypeLabel where
+--     show WrongTypeLabel =
+--         _ERROR <> ": Mislabelled type lambda
+--         \                                                                                \n\
+--         \Expected your t provide an extract function that succeeds if an expression      \n\
+--         \matches the expected type.  You provided a Type that disobeys this contract     \n"