TMap, Every and nice type level things, helpful for servant, hspec, etc.

tmap.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module TypeLevel where

import Control.Applicative
import Data.Aeson
import Data.Functor.Contravariant (Op(..))
import Data.Proxy
import Data.Swagger
import Data.Typeable
import Test.Hspec
import Test.Hspec.QuickCheck
import Test.QuickCheck
import GHC.Exts (Constraint)
import Servant

-- $setup
-- >>> :set -XDataKinds
-- >>> :set -XFlexibleContexts
-- >>> :set -XGADTs
-- >>> :set -XRankNTypes
-- >>> :set -XScopedTypeVariables
-- >>> import GHC.TypeLits
-- >>> import Data.List

-- | Map a list of constrained types to a list of values.
--
-- >>> tmap (Proxy :: Proxy KnownSymbol) symbolVal (Proxy :: Proxy ["hello", "world"])
-- ["hello","world"]
class TMap (q :: k -> Constraint) (xs :: [k]) where
  tmap :: p q -> (forall x p'. q x => p' x -> a) -> p'' xs -> [a]

instance TMap q '[] where
  tmap _ _ _ = []

instance (q x, TMap q xs) => TMap q (x ': xs) where
  tmap q f _ = f (Proxy :: Proxy x) : tmap q f (Proxy :: Proxy xs)

-- | Apply multiple constraint constructors to a type.
--
-- @
-- EveryTF '[Show, Read] a ~ (Show a, Read a)
-- @
--
-- Note that since this is a type family, you have to alway fully apply @'EveryTF'@.
--
-- For partial application of multiple constraint constructors see @'Every'@.
type family EveryTF cs x :: Constraint where
  EveryTF '[] x = ()
  EveryTF (c ': cs) x = (c x, EveryTF cs x)

-- | @'EveryProof' cs x@ is a proof that @x@ satisfies all constraints in @cs@.
--
-- E.g. a value of type @'EveryProof' '[Show, Read] a@ proves that @a@ has both @Show@ and @Read@ instances.
--
-- Pattern matching on @'EveryProofCons'@ brings one constraint at a time to the scope.
data EveryProof cs x where
  EveryProofNil  :: EveryProof '[] x
  EveryProofCons :: c x => EveryProof cs x -> EveryProof (c ': cs) x

-- | Apply multiple constraint constructors to a type as a class.
--
-- This is different from @'EveryTF'@ in that it allows partial application.
-- However, @'Every' cs@ does not immediately bring @'EveryTF'@ into scope, so you
-- can't use the instances right away:
--
-- >>> :{
-- let f :: Every [Show, Num] a => a -> String
--     f = show
-- :}
-- ...
--     Could not deduce (Show a) arising from a use of ‘show’
--     from the context (Every '[Show, Num] a)
-- ...
--
-- To bring individual constraints into scope use @'every'@ and pattern match on the proof:
--
-- >>> :{
-- let f :: forall a. Every [Show, Num] a => a -> String
--     f = case (every :: EveryProof [Show, Num] a) of EveryProofCons (EveryProofCons EveryProofNil) -> show
-- in f 123
-- :}
-- "123"
--
-- Alternatively, you can use @'appWith'@ to convert @'Every' cs@ constraint into @'EveryTF' cs@.
-- @'appWith' pqs pcs f px@ applies a function @f@ with regular constraints to a proxied type @px@,
-- using @'Every' cs x@ constraint of @px@. It automatically proves that @px@ satisfies the
-- regular constraints of @f@.
--
-- >>> let num = Proxy :: Proxy '[Num]
-- >>> let enumOrd = Proxy :: Proxy '[Enum, Ord]
-- >>> let xs :: (Num a, Enum a, Ord a) => p a -> [a]; xs _ = sort [1, 4, 3, 2]
-- >>> let ys :: (Num a, Every '[Enum, Ord] a) => p a -> [a]; ys = appWith num enumOrd xs
-- >>> ys (Proxy :: Proxy Int)
-- [1,2,3,4]
--
-- It might be useful to look at the type of @'appWith'@ also like this:
--
-- @
-- appWith :: pq qs -> p cs
--    -> (forall x p'. (EveryTF qs x, EveryTF cs x) => p' x -> f x)
--    -> (forall x p'. (EveryTF qs x, Every   cs x) => p' x -> f x)
-- @
class Every (cs :: [* -> Constraint]) (x :: *) where
  every :: EveryProof cs x
  appWith :: EveryTF qs x => pq qs -> p cs -> (forall x p'. (EveryTF qs x, EveryTF cs x) => p' x -> f x) -> p'' x -> f x

instance Every '[] x where
  every = EveryProofNil
  appWith _ _ f x = f x

instance (c x, Every cs x) => Every (c ': cs) x where
  every = EveryProofCons every

  appWith :: forall qs pq p p'' a f. EveryTF qs x => pq qs -> p (c ': cs) -> (forall x p'. (EveryTF (c ': cs) x, EveryTF qs x) => p' x -> f x) -> p'' x -> f x
  appWith q _ f px = case (every :: EveryProof (c ': cs) x) of
    EveryProofCons r -> appWith (Proxy :: Proxy (c ': qs)) (Proxy :: Proxy cs) f px

-- | Convert some constraints from @'Every'@ to @'EveryTF'@
-- for a function which result type does not depend on its argument's type.
appWith_ :: (EveryTF qs x, Every cs x) => pq qs -> p cs -> (forall x p'. (EveryTF qs x, EveryTF cs x) => p' x -> a) -> p'' x -> a
appWith_ q p f = getConst . appWith q p (\p' -> Const (f p'))

-- | Convert all constraints from @'Every'@ to @'EveryTF'@.
app :: Every cs x => p cs -> (forall x p'. EveryTF cs x => p' x -> f x) -> p'' x -> f x
app = appWith (Proxy :: Proxy '[])

-- | Convert all constraints from @'Every'@ to @'EveryTF'@
-- for a function which result type does not depend on its argument's type.
app_ :: Every cs x => p cs -> (forall x p'. EveryTF cs x => p' x -> a) -> p'' x -> a
app_ p f = getConst . app p (\p' -> Const (f p'))

-- | Convert all constraints from @'Every'@ to @'EveryTF'@
-- for a term-level function which result type does not depend on its argument's type.
appVal_ :: forall p a cs x. Every cs x => p cs -> (forall x. EveryTF cs x => x -> a) -> x -> a
appVal_ p f = getOp (app p f' (Proxy :: Proxy x))
  where
    f' :: forall p y. EveryTF cs y => p y -> Op a y
    f' _ = Op f

-- | Like @'tmap'@, but uses @'Every'@ for multiple constraints.
--
-- >>> let zero :: forall p a. (Show a, Num a) => p a -> String; zero _ = show (0 :: a)
-- >>> tmapEvery (Proxy :: Proxy [Show, Num]) zero (Proxy :: Proxy [Int, Float])
-- ["0","0.0"]
tmapEvery :: forall a cs p p'' xs. (TMap (Every cs) xs) =>
  p cs -> (forall x p'. EveryTF cs x => p' x -> a) -> p'' xs -> [a]
tmapEvery pcs f = tmap (Proxy :: Proxy (Every cs)) (app_ pcs f)

-- * QuickCheck-related stuff

-- | Construct property tests for each type in a list.
-- The name for each property is the name of the corresponding type.
--
-- >>> :{
--  hspec $
--    context "read . show == id" $
--      props
--        (Proxy :: Proxy [Eq, Show, Read])
--        (\x -> read (show x) == x)
--        (Proxy :: Proxy [Bool, Int, String])
-- :}
-- <BLANKLINE>
-- read . show == id
--   Bool
--   Int
--   [Char]
-- <BLANKLINE>
-- Finished in ... seconds
-- 3 examples, 0 failures
props :: forall p p' p'' cs xs. TMap (Every (Typeable ': Show ': Arbitrary ': cs)) xs =>
  p cs -> (forall x p'. EveryTF cs x => x -> Bool) -> p'' xs -> Spec
props _ f px = sequence_ specs
  where
    specs :: [Spec]
    specs = tmapEvery (Proxy :: Proxy (Typeable ': Show ': Arbitrary ': cs)) aprop px

    aprop :: forall p a. (EveryTF cs a, Typeable a, Show a, Arbitrary a) => p a -> Spec
    aprop _ = prop (show (typeOf (undefined :: a))) (f :: a -> Bool)

-- * Servant-related stuff

type family X api :: [*]
type instance X (Get cs a) = '[a]
type instance X (ReqBody cs a :> api) = a ': X api

validateEveryToJSON :: forall proxy api. TMap (Every [Typeable, Show, Arbitrary, ToJSON, ToSchema]) (X api) => proxy api -> Spec
validateEveryToJSON _ = props (Proxy :: Proxy [ToJSON, ToSchema]) (\x -> validateToJSON x == []) (Proxy :: Proxy (X api))

validateToJSON :: (ToJSON a, ToSchema a) => a -> [String]
validateToJSON = undefined