Safe Haskell | None |
---|---|
Language | Haskell2010 |
This module exposes unsafe refinements. An unsafe refinement
is one which either does not make the guarantee of totality in construction
of the Refined
value or does not perform a check of the refinement
predicate. It is recommended only to use this when you can manually prove
that the refinement predicate holds.
Synopsis
- data Refined (p :: k) x
- reallyUnsafeRefine :: x -> Refined p x
- unsafeRefine :: Predicate p x => x -> Refined p x
- reallyUnsafeUnderlyingRefined :: Coercion x (Refined p x)
- reallyUnsafeAllUnderlyingRefined :: ((forall x y p. Coercible x y => Coercible y (Refined p x)) => r) -> r
- reallyUnsafePredEquiv :: Coercion (Refined p x) (Refined q x)
Refined
data Refined (p :: k) x Source #
A refinement type, which wraps a value of type x
.
Since: 0.1.0.0
Instances
Lift x => Lift (Refined p x :: Type) Source # | Since: 0.1.0.0 |
Foldable (Refined p) Source # | Since: 0.2 |
Defined in Refined.Unsafe.Type fold :: Monoid m => Refined p m -> m # foldMap :: Monoid m => (a -> m) -> Refined p a -> m # foldMap' :: Monoid m => (a -> m) -> Refined p a -> m # foldr :: (a -> b -> b) -> b -> Refined p a -> b # foldr' :: (a -> b -> b) -> b -> Refined p a -> b # foldl :: (b -> a -> b) -> b -> Refined p a -> b # foldl' :: (b -> a -> b) -> b -> Refined p a -> b # foldr1 :: (a -> a -> a) -> Refined p a -> a # foldl1 :: (a -> a -> a) -> Refined p a -> a # toList :: Refined p a -> [a] # length :: Refined p a -> Int # elem :: Eq a => a -> Refined p a -> Bool # maximum :: Ord a => Refined p a -> a # minimum :: Ord a => Refined p a -> a # | |
Eq x => Eq (Refined p x) Source # | Since: 0.1.0.0 |
Ord x => Ord (Refined p x) Source # | Since: 0.1.0.0 |
Defined in Refined.Unsafe.Type | |
(Read x, Predicate p x) => Read (Refined p x) Source # | This instance makes sure to check the refinement. Since: 0.1.0.0 |
Show x => Show (Refined p x) Source # | Since: 0.1.0.0 |
(Arbitrary a, Typeable a, Typeable p, Predicate p a) => Arbitrary (Refined p a) Source # | Since: 0.4 |
Hashable x => Hashable (Refined p x) Source # | Since: 0.6.3 |
Defined in Refined.Unsafe.Type | |
(ToJSON a, Predicate p a) => ToJSON (Refined p a) Source # | Since: 0.4 |
(ToJSONKey a, Predicate p a) => ToJSONKey (Refined p a) Source # | Since: 0.6.3 |
Defined in Refined toJSONKey :: ToJSONKeyFunction (Refined p a) # toJSONKeyList :: ToJSONKeyFunction [Refined p a] # | |
(FromJSON a, Predicate p a) => FromJSON (Refined p a) Source # | Since: 0.4 |
(FromJSONKey a, Predicate p a) => FromJSONKey (Refined p a) Source # | |
Defined in Refined fromJSONKey :: FromJSONKeyFunction (Refined p a) # fromJSONKeyList :: FromJSONKeyFunction [Refined p a] # | |
NFData x => NFData (Refined p x) Source # | Since: 0.5 |
Defined in Refined.Unsafe.Type |
Creation
reallyUnsafeRefine :: x -> Refined p x Source #
Constructs a Refined
value, completely
ignoring any refinements! Use this only
when you can manually prove that the refinement
holds.
Since: 0.3.0.0
unsafeRefine :: Predicate p x => x -> Refined p x Source #
Coercion
reallyUnsafeUnderlyingRefined :: Coercion x (Refined p x) Source #
A coercion between a type and any refinement of that type. See Data.Type.Coercion for functions manipulating coercions.
Since: 0.3.0.0