src/Webc/Data.hs

   1 -- For the Route pattern
   2 {-# LANGUAGE PatternSynonyms #-}
   3 -- For the Route pattern
   4 {-# LANGUAGE ViewPatterns #-}
   5
   6 module Webc.Data where
   7
   8 import Data.Kind (Constraint, Type)
   9 import Data.Maybe (Maybe (..))
  10 import Symantic.Derive (Derivable (..), Derived)
  11 import Type.Reflection (Typeable, eqTypeRep, typeRep, (:~~:) (..))
  12
  13 -- * Type 'Route'
  14
  15 {- | Pattern-matchable combinators (initial algebra) for routes.
  16  This is an extensible data-type indexed by
  17  the symantic classes (final algebra).
  18 -}
  19 data family
  20   Route
  21     (route :: (Type -> Type) -> Constraint) ::
  22     (Type -> Type) -> (Type -> Type)
  23
  24 type instance Derived (Route route repr) = repr
  25
  26 -- ** Type 'SomeRoute'
  27
  28 {- | Some 'Route' existentialized over
  29  the actual indexing symantic class.
  30  Useful for the initial algebra of symantic combinators
  31  containing at least one 'Route'.
  32 -}
  33 data SomeRoute repr a
  34   = forall route.
  35     ( Derivable (Route route repr)
  36     , Typeable route
  37     ) =>
  38     SomeRoute (Route route repr a)
  39
  40 {- | Convenient utility to pattern-match a 'SomeRoute'.
  41  and bring its constraints in scope.
  42 -}
  43 pattern Route :: Typeable route => Route route repr a -> SomeRoute repr a
  44 pattern Route x <- (unSomeRoute -> Just x)
  45
  46 {- | @(unSomeRoute x :: 'Maybe' ('Route' route repr a))@
  47  extract the data-constructor from the given 'SomeRoute'
  48  iif. it belongs to the @('Route' route repr a)@ data-instance.
  49 -}
  50 unSomeRoute ::
  51   forall route repr a.
  52   Typeable route =>
  53   SomeRoute repr a ->
  54   Maybe (Route route repr a)
  55 unSomeRoute (SomeRoute (x :: Route x repr a)) =
  56   case typeRep @route `eqTypeRep` typeRep @x of
  57     Just HRefl -> Just x
  58     Nothing -> Nothing
  59
  60 type instance Derived (SomeRoute repr) = repr
  61 instance Derivable (SomeRoute repr) where
  62   derive (SomeRoute x) = derive x