Predicate.hs (1140B)
1 {-# LANGUAGE IncoherentInstances #-} 2 3 module Lude.Constraint.Predicate ( 4 -- AllSatisfy, 5 Always, 6 always, 7 Never, 8 never, 9 ) where 10 11 import Lude.Constraint.Falsum 12 import Lude.Haskell 13 14 -- TODO: I don't like this organization. Why isn't Always/Never treated the 15 -- same as Verum/Falsum? These can probably just be terminal/initial objects 16 -- in a functor category. 17 18 -------------------------------------------------------------------------------- 19 20 -- type AllSatisfy :: forall {i}. Predicate i -> List i -> Constraint 21 -- type family AllSatisfy p xs where 22 -- AllSatisfy _ [] = Verum 23 -- AllSatisfy p (x : xs) = p x & AllSatisfy p xs 24 25 -------------------------------------------------------------------------------- 26 27 type role Always phantom 28 type Always :: forall {i}. Predicate i 29 class Always x 30 instance forall x. Always x 31 32 always :: forall a x. a :- Always x 33 always = Entail MkEvidence 34 35 -------------------------------------------------------------------------------- 36 37 type role Never phantom 38 type Never :: forall {i}. Predicate i 39 class (Falsum) => Never x 40 41 never :: forall x a. Never x :- a 42 never = Entail contradiction