module Exinst.Singletons
(
Some1(Some1)
, some1
, withSome1Sing
, withSome1
, fromSome1
, Dict1(dict1)
, Some2(Some2)
, some2
, withSome2Sing
, withSome2
, fromSome2
, Dict2(dict2)
, Some3(Some3)
, some3
, withSome3Sing
, withSome3
, fromSome3
, Dict3(dict3)
, Some4(Some4)
, some4
, withSome4Sing
, withSome4
, fromSome4
, Dict4(dict4)
, Dict(Dict)
) where
import Data.Constraint
import Data.Singletons
import Data.Singletons.Decide
import Data.Type.Equality
import Prelude
data Some1 (f1 :: k1 -> *) = forall a1.
Some1 !(Sing a1) !(f1 a1)
data Some2 (f2 :: k2 -> k1 -> *) = forall a2 a1.
Some2 !(Sing a2) !(Sing a1) !(f2 a2 a1)
data Some3 (f3 :: k3 -> k2 -> k1 -> *) = forall a3 a2 a1.
Some3 !(Sing a3) !(Sing a2) !(Sing a1) !(f3 a3 a2 a1)
data Some4 (f4 :: k4 -> k3 -> k2 -> k1 -> *) = forall a4 a3 a2 a1.
Some4 !(Sing a4) !(Sing a3) !(Sing a2) !(Sing a1) !(f4 a4 a3 a2 a1)
some1
:: forall (f1 :: k1 -> *) a1
. SingI a1
=> f1 a1
-> Some1 f1
some1 = Some1 (sing :: Sing a1)
some2
:: forall (f2 :: k2 -> k1 -> *) a2 a1
. (SingI a2, SingI a1)
=> f2 a2 a1
-> Some2 f2
some2 = Some2 (sing :: Sing a2) (sing :: Sing a1)
some3
:: forall (f3 :: k3 -> k2 -> k1 -> *) a3 a2 a1
. (SingI a3, SingI a2, SingI a1)
=> f3 a3 a2 a1
-> Some3 f3
some3 = Some3 (sing :: Sing a3) (sing :: Sing a2) (sing :: Sing a1)
some4
:: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) a4 a3 a2 a1
. (SingI a4, SingI a3, SingI a2, SingI a1)
=> f4 a4 a3 a2 a1
-> Some4 f4
some4 = Some4 (sing :: Sing a4) (sing :: Sing a3)
(sing :: Sing a2) (sing :: Sing a1)
withSome1
:: forall (f1 :: k1 -> *) (r :: *)
. Some1 f1
-> (forall a1. SingI a1 => f1 a1 -> r)
-> r
withSome1 s1 g = withSome1Sing s1 (\_ -> g)
withSome2
:: forall (f2 :: k2 -> k1 -> *) (r :: *)
. Some2 f2
-> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r)
-> r
withSome2 s2 g = withSome2Sing s2 (\_ _ -> g)
withSome3
:: forall (f3 :: k3 -> k2 -> k1 -> *) (r :: *)
. Some3 f3
-> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r)
-> r
withSome3 s3 g = withSome3Sing s3 (\_ _ _ -> g)
withSome4
:: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) (r :: *)
. Some4 f4
-> (forall a4 a3 a2 a1
. (SingI a4, SingI a3, SingI a2, SingI a1)
=> f4 a4 a3 a2 a1 -> r)
-> r
withSome4 s4 g = withSome4Sing s4 (\_ _ _ _ -> g)
withSome1Sing
:: forall (f1 :: k1 -> *) (r :: *)
. Some1 f1
-> (forall a1. (SingI a1) => Sing a1 -> f1 a1 -> r)
-> r
withSome1Sing (Some1 sa1 x) g = withSingI sa1 (g sa1 x)
withSome2Sing
:: forall (f2 :: k2 -> k1 -> *) (r :: *)
. Some2 f2
-> (forall a2 a1. (SingI a2, SingI a1) => Sing a2 -> Sing a1 -> f2 a2 a1 -> r)
-> r
withSome2Sing (Some2 sa2 sa1 x) g = withSingI sa2 (withSingI sa1 (g sa2 sa1 x))
withSome3Sing
:: forall (f3 :: k3 -> k2 -> k1 -> *) (r :: *)
. Some3 f3
-> (forall a3 a2 a1
. (SingI a3, SingI a2, SingI a1)
=> Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)
-> r
withSome3Sing (Some3 sa3 sa2 sa1 x) g =
withSingI sa3 (withSingI sa2 (withSingI sa1 (g sa3 sa2 sa1 x)))
withSome4Sing
:: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) (r :: *)
. Some4 f4
-> (forall a4 a3 a2 a1
. (SingI a4, SingI a3, SingI a2, SingI a1)
=> Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)
-> r
withSome4Sing (Some4 sa4 sa3 sa2 sa1 x) g =
withSingI sa4 (withSingI sa3 (withSingI sa2 (withSingI sa1
(g sa4 sa3 sa2 sa1 x))))
fromSome1
:: forall (f1 :: k1 -> *) a1
. (SingI a1, SDecide ('KProxy :: KProxy k1))
=> Some1 f1
-> Maybe (f1 a1)
fromSome1 = \(Some1 sa1' x) -> do
Refl <- testEquality sa1' (sing :: Sing a1)
return x
fromSome2
:: forall (f2 :: k2 -> k1 -> *) a2 a1
. ( SingI a2, SDecide ('KProxy :: KProxy k2)
, SingI a1, SDecide ('KProxy :: KProxy k1))
=> Some2 f2
-> Maybe (f2 a2 a1)
fromSome2 = \(Some2 sa2' sa1' x) -> do
Refl <- testEquality sa2' (sing :: Sing a2)
Refl <- testEquality sa1' (sing :: Sing a1)
return x
fromSome3
:: forall (f3 :: k3 -> k2 -> k1 -> *) a3 a2 a1
. ( SingI a3, SDecide ('KProxy :: KProxy k3)
, SingI a2, SDecide ('KProxy :: KProxy k2)
, SingI a1, SDecide ('KProxy :: KProxy k1))
=> Some3 f3
-> Maybe (f3 a3 a2 a1)
fromSome3 = \(Some3 sa3' sa2' sa1' x) -> do
Refl <- testEquality sa3' (sing :: Sing a3)
Refl <- testEquality sa2' (sing :: Sing a2)
Refl <- testEquality sa1' (sing :: Sing a1)
return x
fromSome4
:: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) a4 a3 a2 a1
. ( SingI a4, SDecide ('KProxy :: KProxy k4)
, SingI a3, SDecide ('KProxy :: KProxy k3)
, SingI a2, SDecide ('KProxy :: KProxy k2)
, SingI a1, SDecide ('KProxy :: KProxy k1))
=> Some4 f4
-> Maybe (f4 a4 a3 a2 a1)
fromSome4 = \(Some4 sa4' sa3' sa2' sa1' x) -> do
Refl <- testEquality sa4' (sing :: Sing a4)
Refl <- testEquality sa3' (sing :: Sing a3)
Refl <- testEquality sa2' (sing :: Sing a2)
Refl <- testEquality sa1' (sing :: Sing a1)
return x
class Dict1 (c :: k0 -> Constraint) (f1 :: k1 -> k0) where
dict1 :: Sing a1 -> Dict (c (f1 a1))
class Dict2 (c :: k0 -> Constraint) (f2 :: k2 -> k1 -> k0) where
dict2 :: Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))
class Dict3 (c :: k0 -> Constraint) (f3 :: k3 -> k2 -> k1 -> k0) where
dict3 :: Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))
class Dict4 (c :: k0 -> Constraint) (f4 :: k4 -> k3 -> k2 -> k1 -> k0) where
dict4 :: Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))