singletons-3.0.1: tests/ByHand.hs
{- ByHand.hs
(c) Richard Eisenberg 2012
rae@cs.brynmawr.edu
Shows the derivations for the singleton definitions done by hand.
This file is a great way to understand the singleton encoding better.
-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors -Wno-orphans #-}
{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures, GADTs,
FlexibleInstances, FlexibleContexts, UndecidableInstances,
RankNTypes, TypeOperators, MultiParamTypeClasses,
FunctionalDependencies, ScopedTypeVariables,
LambdaCase, EmptyCase,
TypeApplications, EmptyCase, CPP #-}
#if __GLASGOW_HASKELL__ < 806
{-# LANGUAGE TypeInType #-}
#endif
#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#endif
module ByHand where
import Data.Kind
import Data.Type.Equality hiding (type (==), apply)
import Data.Proxy
import Data.Singletons
import Data.Singletons.Decide
import Prelude hiding ((+), (-), map, zipWith)
import Unsafe.Coerce
-----------------------------------
-- Original ADTs ------------------
-----------------------------------
#if __GLASGOW_HASKELL__ >= 810
type Nat :: Type
#endif
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
deriving Eq
-- Defined using names to avoid fighting with concrete syntax
#if __GLASGOW_HASKELL__ >= 810
type List :: Type -> Type
#endif
data List :: Type -> Type where
Nil :: List a
Cons :: a -> List a -> List a
deriving Eq
-----------------------------------
-- One-time definitions -----------
-----------------------------------
-- Promoted equality type class
#if __GLASGOW_HASKELL__ >= 810
type PEq :: Type -> Constraint
#endif
class PEq k where
type (==) (a :: k) (b :: k) :: Bool
-- omitting definition of /=
-- Singleton type equality type class
#if __GLASGOW_HASKELL__ >= 810
type SEq :: Type -> Constraint
#endif
class SEq k where
(%==) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Sing (a == b)
-- omitting definition of %/=
#if __GLASGOW_HASKELL__ >= 810
type If :: Bool -> a -> a -> a
#endif
type family If (cond :: Bool) (tru :: a) (fls :: a) :: a where
If True tru fls = tru
If False tru fls = fls
sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
sIf STrue b _ = b
sIf SFalse _ c = c
-----------------------------------
-- Auto-generated code ------------
-----------------------------------
-- Nat
#if __GLASGOW_HASKELL__ >= 810
type SNat :: Nat -> Type
#endif
data SNat :: Nat -> Type where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
type instance Sing = SNat
#if __GLASGOW_HASKELL__ >= 810
type SuccSym0 :: Nat ~> Nat
#endif
data SuccSym0 :: Nat ~> Nat
type instance Apply SuccSym0 x = Succ x
#if __GLASGOW_HASKELL__ >= 810
type EqualsNat :: Nat -> Nat -> Bool
#endif
type family EqualsNat (a :: Nat) (b :: Nat) :: Bool where
EqualsNat Zero Zero = True
EqualsNat (Succ a) (Succ b) = a == b
EqualsNat (n1 :: Nat) (n2 :: Nat) = False
instance PEq Nat where
type a == b = EqualsNat a b
instance SEq Nat where
SZero %== SZero = STrue
SZero %== (SSucc _) = SFalse
(SSucc _) %== SZero = SFalse
(SSucc n) %== (SSucc n') = n %== n'
instance SDecide Nat where
SZero %~ SZero = Proved Refl
(SSucc m) %~ (SSucc n) =
case m %~ n of
Proved Refl -> Proved Refl
Disproved contra -> Disproved (\Refl -> contra Refl)
SZero %~ (SSucc _) = Disproved (\case)
(SSucc _) %~ SZero = Disproved (\case)
instance SingI Zero where
sing = SZero
instance SingI n => SingI (Succ n) where
sing = SSucc sing
instance SingI1 Succ where
liftSing = SSucc
instance SingKind Nat where
type Demote Nat = Nat
fromSing SZero = Zero
fromSing (SSucc n) = Succ (fromSing n)
toSing Zero = SomeSing SZero
toSing (Succ n) = withSomeSing n (\n' -> SomeSing $ SSucc n')
-- Bool
#if __GLASGOW_HASKELL__ >= 810
type SBool :: Bool -> Type
#endif
data SBool :: Bool -> Type where
SFalse :: SBool False
STrue :: SBool True
type instance Sing = SBool
{-
(&&) :: Bool -> Bool -> Bool
False && _ = False
True && x = x
-}
#if __GLASGOW_HASKELL__ >= 810
type (&&) :: Bool -> Bool -> Bool
#endif
type family (a :: Bool) && (b :: Bool) :: Bool where
False && _ = False
True && x = x
(%&&) :: forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a && b)
SFalse %&& SFalse = SFalse
SFalse %&& STrue = SFalse
STrue %&& SFalse = SFalse
STrue %&& STrue = STrue
instance SingI False where
sing = SFalse
instance SingI True where
sing = STrue
instance SingKind Bool where
type Demote Bool = Bool
fromSing SFalse = False
fromSing STrue = True
toSing False = SomeSing SFalse
toSing True = SomeSing STrue
-- Maybe
#if __GLASGOW_HASKELL__ >= 810
type SMaybe :: forall k. Maybe k -> Type
#endif
data SMaybe :: forall k. Maybe k -> Type where
SNothing :: SMaybe Nothing
SJust :: forall k (a :: k). Sing a -> SMaybe (Just a)
type instance Sing = SMaybe
#if __GLASGOW_HASKELL__ >= 810
type EqualsMaybe :: Maybe k -> Maybe k -> Bool
#endif
type family EqualsMaybe (a :: Maybe k) (b :: Maybe k) :: Bool where
EqualsMaybe Nothing Nothing = True
EqualsMaybe (Just a) (Just a') = a == a'
EqualsMaybe (x :: Maybe k) (y :: Maybe k) = False
instance PEq a => PEq (Maybe a) where
type m1 == m2 = EqualsMaybe m1 m2
instance SDecide k => SDecide (Maybe k) where
SNothing %~ SNothing = Proved Refl
(SJust x) %~ (SJust y) =
case x %~ y of
Proved Refl -> Proved Refl
Disproved contra -> Disproved (\Refl -> contra Refl)
SNothing %~ (SJust _) = Disproved (\case)
(SJust _) %~ SNothing = Disproved (\case)
instance SEq k => SEq (Maybe k) where
SNothing %== SNothing = STrue
SNothing %== (SJust _) = SFalse
(SJust _) %== SNothing = SFalse
(SJust a) %== (SJust a') = a %== a'
instance SingI (Nothing :: Maybe k) where
sing = SNothing
instance SingI a => SingI (Just (a :: k)) where
sing = SJust sing
instance SingI1 Just where
liftSing = SJust
instance SingKind k => SingKind (Maybe k) where
type Demote (Maybe k) = Maybe (Demote k)
fromSing SNothing = Nothing
fromSing (SJust a) = Just (fromSing a)
toSing Nothing = SomeSing SNothing
toSing (Just x) =
case toSing x :: SomeSing k of
SomeSing x' -> SomeSing $ SJust x'
-- List
#if __GLASGOW_HASKELL__ >= 810
type SList :: forall k. List k -> Type
#endif
data SList :: forall k. List k -> Type where
SNil :: SList Nil
SCons :: forall k (h :: k) (t :: List k). Sing h -> SList t -> SList (Cons h t)
type instance Sing = SList
#if __GLASGOW_HASKELL__ >= 810
type NilSym0 :: List a
#endif
type family NilSym0 :: List a where
NilSym0 = Nil
#if __GLASGOW_HASKELL__ >= 810
type ConsSym0 :: forall a. a ~> List a ~> List a
type ConsSym1 :: forall a. a -> List a ~> List a
type ConsSym2 :: forall a. a -> List a -> List a
#endif
data ConsSym0 :: forall a. a ~> List a ~> List a
data ConsSym1 :: forall a. a -> List a ~> List a
type family ConsSym2 (x :: a) (y :: List a) :: List a where
ConsSym2 x y = Cons x y
type instance Apply ConsSym0 a = ConsSym1 a
type instance Apply (ConsSym1 a) b = Cons a b
#if __GLASGOW_HASKELL__ >= 810
type EqualsList :: List k -> List k -> Bool
#endif
type family EqualsList (a :: List k) (b :: List k) :: Bool where
EqualsList Nil Nil = True
EqualsList (Cons a b) (Cons a' b') = (a == a') && (b == b')
EqualsList (x :: List k) (y :: List k) = False
instance PEq a => PEq (List a) where
type l1 == l2 = EqualsList l1 l2
instance SEq k => SEq (List k) where
SNil %== SNil = STrue
SNil %== (SCons _ _) = SFalse
(SCons _ _) %== SNil = SFalse
(SCons a b) %== (SCons a' b') = (a %== a') %&& (b %== b')
instance SDecide k => SDecide (List k) where
SNil %~ SNil = Proved Refl
(SCons h1 t1) %~ (SCons h2 t2) =
case (h1 %~ h2, t1 %~ t2) of
(Proved Refl, Proved Refl) -> Proved Refl
(Disproved contra, _) -> Disproved (\Refl -> contra Refl)
(_, Disproved contra) -> Disproved (\Refl -> contra Refl)
SNil %~ (SCons _ _) = Disproved (\case)
(SCons _ _) %~ SNil = Disproved (\case)
instance SingI Nil where
sing = SNil
instance (SingI h, SingI t) =>
SingI (Cons (h :: k) (t :: List k)) where
sing = SCons sing sing
instance SingI h => SingI1 (Cons (h :: k)) where
liftSing = SCons sing
instance SingI2 Cons where
liftSing2 = SCons
instance SingKind k => SingKind (List k) where
type Demote (List k) = List (Demote k)
fromSing SNil = Nil
fromSing (SCons h t) = Cons (fromSing h) (fromSing t)
toSing Nil = SomeSing SNil
toSing (Cons h t) =
case ( toSing h :: SomeSing k
, toSing t :: SomeSing (List k) ) of
(SomeSing h', SomeSing t') -> SomeSing $ SCons h' t'
-- Either
#if __GLASGOW_HASKELL__ >= 810
type SEither :: forall k1 k2. Either k1 k2 -> Type
#endif
data SEither :: forall k1 k2. Either k1 k2 -> Type where
SLeft :: forall k1 (a :: k1). Sing a -> SEither (Left a)
SRight :: forall k2 (b :: k2). Sing b -> SEither (Right b)
type instance Sing = SEither
instance (SingI a) => SingI (Left (a :: k)) where
sing = SLeft sing
instance SingI1 Left where
liftSing = SLeft
instance (SingI b) => SingI (Right (b :: k)) where
sing = SRight sing
instance SingI1 Right where
liftSing = SRight
instance (SingKind k1, SingKind k2) => SingKind (Either k1 k2) where
type Demote (Either k1 k2) = Either (Demote k1) (Demote k2)
fromSing (SLeft x) = Left (fromSing x)
fromSing (SRight x) = Right (fromSing x)
toSing (Left x) =
case toSing x :: SomeSing k1 of
SomeSing x' -> SomeSing $ SLeft x'
toSing (Right x) =
case toSing x :: SomeSing k2 of
SomeSing x' -> SomeSing $ SRight x'
instance (SDecide k1, SDecide k2) => SDecide (Either k1 k2) where
(SLeft x) %~ (SLeft y) =
case x %~ y of
Proved Refl -> Proved Refl
Disproved contra -> Disproved (\Refl -> contra Refl)
(SRight x) %~ (SRight y) =
case x %~ y of
Proved Refl -> Proved Refl
Disproved contra -> Disproved (\Refl -> contra Refl)
(SLeft _) %~ (SRight _) = Disproved (\case)
(SRight _) %~ (SLeft _) = Disproved (\case)
-- Composite
#if __GLASGOW_HASKELL__ >= 810
type Composite :: Type -> Type -> Type
#endif
data Composite :: Type -> Type -> Type where
MkComp :: Either (Maybe a) b -> Composite a b
#if __GLASGOW_HASKELL__ >= 810
type SComposite :: forall k1 k2. Composite k1 k2 -> Type
#endif
data SComposite :: forall k1 k2. Composite k1 k2 -> Type where
SMkComp :: forall k1 k2 (a :: Either (Maybe k1) k2). SEither a -> SComposite (MkComp a)
type instance Sing = SComposite
instance SingI a => SingI (MkComp (a :: Either (Maybe k1) k2)) where
sing = SMkComp sing
instance SingI1 MkComp where
liftSing = SMkComp
instance (SingKind k1, SingKind k2) => SingKind (Composite k1 k2) where
type Demote (Composite k1 k2) =
Composite (Demote k1) (Demote k2)
fromSing (SMkComp x) = MkComp (fromSing x)
toSing (MkComp x) =
case toSing x :: SomeSing (Either (Maybe k1) k2) of
SomeSing x' -> SomeSing $ SMkComp x'
instance (SDecide k1, SDecide k2) => SDecide (Composite k1 k2) where
(SMkComp x) %~ (SMkComp y) =
case x %~ y of
Proved Refl -> Proved Refl
Disproved contra -> Disproved (\Refl -> contra Refl)
-- Empty
#if __GLASGOW_HASKELL__ >= 810
type Empty :: Type
#endif
data Empty
#if __GLASGOW_HASKELL__ >= 810
type SEmpty :: Empty -> Type
#endif
data SEmpty :: Empty -> Type
type instance Sing = SEmpty
instance SingKind Empty where
type Demote Empty = Empty
fromSing = \case
toSing x = SomeSing (case x of)
-- Type
#if __GLASGOW_HASKELL__ >= 810
type Vec :: Type -> Nat -> Type
#endif
data Vec :: Type -> Nat -> Type where
VNil :: Vec a Zero
VCons :: a -> Vec a n -> Vec a (Succ n)
#if __GLASGOW_HASKELL__ >= 810
type Rep :: Type
#endif
data Rep = Nat | Maybe Rep | Vec Rep Nat
#if __GLASGOW_HASKELL__ >= 810
type SRep :: Type -> Type
#endif
data SRep :: Type -> Type where
SNat :: SRep Nat
SMaybe :: SRep a -> SRep (Maybe a)
SVec :: SRep a -> SNat n -> SRep (Vec a n)
type instance Sing = SRep
instance SingI Nat where
sing = SNat
instance SingI a => SingI (Maybe a) where
sing = SMaybe sing
instance SingI1 Maybe where
liftSing = SMaybe
instance (SingI a, SingI n) => SingI (Vec a n) where
sing = SVec sing sing
instance SingI a => SingI1 (Vec a) where
liftSing = SVec sing
instance SingI2 Vec where
liftSing2 = SVec
instance SingKind Type where
type Demote Type = Rep
fromSing SNat = Nat
fromSing (SMaybe a) = Maybe (fromSing a)
fromSing (SVec a n) = Vec (fromSing a) (fromSing n)
toSing Nat = SomeSing SNat
toSing (Maybe a) =
case toSing a :: SomeSing Type of
SomeSing a' -> SomeSing $ SMaybe a'
toSing (Vec a n) =
case ( toSing a :: SomeSing Type
, toSing n :: SomeSing Nat) of
(SomeSing a', SomeSing n') -> SomeSing $ SVec a' n'
instance SDecide Type where
SNat %~ SNat = Proved Refl
SNat %~ (SMaybe {}) = Disproved (\case)
SNat %~ (SVec {}) = Disproved (\case)
(SMaybe {}) %~ SNat = Disproved (\case)
(SMaybe a) %~ (SMaybe b) =
case a %~ b of
Proved Refl -> Proved Refl
Disproved contra -> Disproved (\Refl -> contra Refl)
(SMaybe {}) %~ (SVec {}) = Disproved (\case)
(SVec {}) %~ SNat = Disproved (\case)
(SVec {}) %~ (SMaybe {}) = Disproved (\case)
(SVec a1 n1) %~ (SVec a2 n2) =
case (a1 %~ a2, n1 %~ n2) of
(Proved Refl, Proved Refl) -> Proved Refl
(Disproved contra, _) -> Disproved (\Refl -> contra Refl)
(_, Disproved contra) -> Disproved (\Refl -> contra Refl)
#if __GLASGOW_HASKELL__ >= 810
type EqualsType :: Type -> Type -> Bool
#endif
type family EqualsType (a :: Type) (b :: Type) :: Bool where
EqualsType a a = True
EqualsType _ _ = False
instance PEq Type where
type a == b = EqualsType a b
instance SEq Type where
a %== b =
case a %~ b of
Proved Refl -> STrue
Disproved _ -> unsafeCoerce SFalse
-----------------------------------
-- Some example functions ---------
-----------------------------------
isJust :: Maybe a -> Bool
isJust Nothing = False
isJust (Just _) = True
#if __GLASGOW_HASKELL__ >= 810
type IsJust :: Maybe k -> Bool
#endif
type family IsJust (a :: Maybe k) :: Bool where
IsJust Nothing = False
IsJust (Just a) = True
-- defunctionalization symbols
#if __GLASGOW_HASKELL__ >= 810
type IsJustSym0 :: forall a. Maybe a ~> Bool
#endif
data IsJustSym0 :: forall a. Maybe a ~> Bool
type instance Apply IsJustSym0 a = IsJust a
sIsJust :: Sing a -> Sing (IsJust a)
sIsJust SNothing = SFalse
sIsJust (SJust _) = STrue
pred :: Nat -> Nat
pred Zero = Zero
pred (Succ n) = n
#if __GLASGOW_HASKELL__ >= 810
type Pred :: Nat -> Nat
#endif
type family Pred (a :: Nat) :: Nat where
Pred Zero = Zero
Pred (Succ n) = n
#if __GLASGOW_HASKELL__ >= 810
type PredSym0 :: Nat ~> Nat
#endif
data PredSym0 :: Nat ~> Nat
type instance Apply PredSym0 a = Pred a
sPred :: forall (t :: Nat). Sing t -> Sing (Pred t)
sPred SZero = SZero
sPred (SSucc n) = n
map :: (a -> b) -> List a -> List b
map _ Nil = Nil
map f (Cons h t) = Cons (f h) (map f t)
#if __GLASGOW_HASKELL__ >= 810
type Map :: (k1 ~> k2) -> List k1 -> List k2
#endif
type family Map (f :: k1 ~> k2) (l :: List k1) :: List k2 where
Map f Nil = Nil
Map f (Cons h t) = Cons (Apply f h) (Map f t)
-- defunctionalization symbols
#if __GLASGOW_HASKELL__ >= 810
type MapSym0 :: forall a b. (a ~> b) ~> List a ~> List b
type MapSym1 :: forall a b. (a ~> b) -> List a ~> List b
#endif
data MapSym0 :: forall a b. (a ~> b) ~> List a ~> List b
data MapSym1 :: forall a b. (a ~> b) -> List a ~> List b
type instance Apply MapSym0 f = MapSym1 f
type instance Apply (MapSym1 f) xs = Map f xs
sMap :: forall k1 k2 (a :: List k1) (f :: k1 ~> k2).
(forall b. Proxy f -> Sing b -> Sing (Apply f b)) -> Sing a -> Sing (Map f a)
sMap _ SNil = SNil
sMap f (SCons h t) = SCons (f Proxy h) (sMap f t)
-- Alternative implementation of sMap with Proxy outside of callback.
-- Not generated by the library.
sMap2 :: forall k1 k2 (a :: List k1) (f :: k1 ~> k2). Proxy f ->
(forall b. Sing b -> Sing (Apply f b)) -> Sing a -> Sing (Map f a)
sMap2 _ _ SNil = SNil
sMap2 p f (SCons h t) = SCons (f h) (sMap2 p f t)
-- test sMap
foo :: Sing (Cons (Succ (Succ Zero)) (Cons (Succ Zero) Nil))
foo = sMap (\(_ :: Proxy (TyCon1 Succ)) -> SSucc) (SCons (SSucc SZero) (SCons SZero SNil))
-- test sMap2
bar :: Sing (Cons (Succ (Succ Zero)) (Cons (Succ Zero) Nil))
bar = sMap2 (Proxy :: Proxy SuccSym0) (SSucc) (SCons (SSucc SZero) (SCons SZero SNil))
baz :: Sing (Cons Zero (Cons Zero Nil))
baz = sMap2 (Proxy :: Proxy PredSym0) (sPred) (SCons (SSucc SZero) (SCons SZero SNil))
zipWith :: (a -> b -> c) -> List a -> List b -> List c
zipWith f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith f xs ys)
zipWith _ Nil (Cons _ _) = Nil
zipWith _ (Cons _ _) Nil = Nil
zipWith _ Nil Nil = Nil
#if __GLASGOW_HASKELL__ >= 810
type ZipWith :: (a ~> b ~> c) -> List a -> List b -> List c
#endif
type family ZipWith (k1 :: a ~> b ~> c) (k2 :: List a) (k3 :: List b) :: List c where
ZipWith f (Cons x xs) (Cons y ys) = Cons (Apply (Apply f x) y) (ZipWith f xs ys)
ZipWith f Nil (Cons z1 z2) = Nil
ZipWith f (Cons z1 z2) Nil = Nil
ZipWith f Nil Nil = Nil
#if __GLASGOW_HASKELL__ >= 810
type ZipWithSym0 :: forall a b c. (a ~> b ~> c) ~> List a ~> List b ~> List c
type ZipWithSym1 :: forall a b c. (a ~> b ~> c) -> List a ~> List b ~> List c
type ZipWithSym2 :: forall a b c. (a ~> b ~> c) -> List a -> List b ~> List c
#endif
data ZipWithSym0 :: forall a b c. (a ~> b ~> c) ~> List a ~> List b ~> List c
data ZipWithSym1 :: forall a b c. (a ~> b ~> c) -> List a ~> List b ~> List c
data ZipWithSym2 :: forall a b c. (a ~> b ~> c) -> List a -> List b ~> List c
type instance Apply ZipWithSym0 f = ZipWithSym1 f
type instance Apply (ZipWithSym1 f) xs = ZipWithSym2 f xs
type instance Apply (ZipWithSym2 f xs) ys = ZipWith f xs ys
sZipWith :: forall a b c (k1 :: a ~> b ~> c) (k2 :: List a) (k3 :: List b).
(forall (t1 :: a). Proxy k1 -> Sing t1 -> forall (t2 :: b). Sing t2 -> Sing (Apply (Apply k1 t1) t2))
-> Sing k2 -> Sing k3 -> Sing (ZipWith k1 k2 k3)
sZipWith f (SCons x xs) (SCons y ys) = SCons (f Proxy x y) (sZipWith f xs ys)
sZipWith _ SNil (SCons _ _) = SNil
sZipWith _ (SCons _ _) SNil = SNil
sZipWith _ SNil SNil = SNil
either :: (a -> c) -> (b -> c) -> Either a b -> c
either l _ (Left x) = l x
either _ r (Right x) = r x
#if __GLASGOW_HASKELL__ >= 810
type Either_ :: (a ~> c) -> (b ~> c) -> Either a b -> c
#endif
type family Either_ (l :: a ~> c) (r :: b ~> c) (e :: Either a b) :: c where
Either_ l r (Left x) = Apply l x
Either_ l r (Right x) = Apply r x
-- defunctionalization symbols
#if __GLASGOW_HASKELL__ >= 810
type Either_Sym0 :: forall a c b. (a ~> c) ~> (b ~> c) ~> Either a b ~> c
type Either_Sym1 :: forall a c b. (a ~> c) -> (b ~> c) ~> Either a b ~> c
type Either_Sym2 :: forall a c b. (a ~> c) -> (b ~> c) -> Either a b ~> c
#endif
data Either_Sym0 :: forall a c b. (a ~> c) ~> (b ~> c) ~> Either a b ~> c
data Either_Sym1 :: forall a c b. (a ~> c) -> (b ~> c) ~> Either a b ~> c
data Either_Sym2 :: forall a c b. (a ~> c) -> (b ~> c) -> Either a b ~> c
type instance Apply Either_Sym0 k1 = Either_Sym1 k1
type instance Apply (Either_Sym1 k1) k2 = Either_Sym2 k1 k2
type instance Apply (Either_Sym2 k1 k2) k3 = Either_ k1 k2 k3
sEither :: forall a b c
(l :: a ~> c)
(r :: b ~> c)
(e :: Either a b).
(forall n. Proxy l -> Sing n -> Sing (Apply l n)) ->
(forall n. Proxy r -> Sing n -> Sing (Apply r n)) ->
Sing e -> Sing (Either_ l r e)
sEither l _ (SLeft x) = l Proxy x
sEither _ r (SRight x) = r Proxy x
-- Alternative implementation of sEither with Proxy outside of callbacks.
-- Not generated by the library.
sEither2 :: forall a b c
(l :: a ~> c)
(r :: b ~> c)
(e :: Either a b).
Proxy l -> Proxy r ->
(forall n. Sing n -> Sing (Apply l n)) ->
(forall n. Sing n -> Sing (Apply r n)) ->
Sing e -> Sing (Either_ l r e)
sEither2 _ _ l _ (SLeft x) = l x
sEither2 _ _ _ r (SRight x) = r x
eitherFoo :: Sing (Succ (Succ Zero))
eitherFoo = sEither (\(_ :: Proxy SuccSym0) -> SSucc)
(\(_ :: Proxy PredSym0) -> sPred) (SLeft (SSucc SZero))
eitherBar :: Sing Zero
eitherBar = sEither2 (Proxy :: Proxy SuccSym0)
(Proxy :: Proxy PredSym0)
SSucc
sPred (SRight (SSucc SZero))
eitherToNat :: Either Nat Nat -> Nat
eitherToNat (Left x) = x
eitherToNat (Right x) = x
#if __GLASGOW_HASKELL__ >= 810
type EitherToNat :: Either Nat Nat -> Nat
#endif
type family EitherToNat (e :: Either Nat Nat) :: Nat where
EitherToNat (Left x) = x
EitherToNat (Right x) = x
sEitherToNat :: Sing a -> Sing (EitherToNat a)
sEitherToNat (SLeft x) = x
sEitherToNat (SRight x) = x
liftMaybe :: (a -> b) -> Maybe a -> Maybe b
liftMaybe _ Nothing = Nothing
liftMaybe f (Just a) = Just (f a)
#if __GLASGOW_HASKELL__ >= 810
type LiftMaybe :: (a ~> b) -> Maybe a -> Maybe b
#endif
type family LiftMaybe (f :: a ~> b) (x :: Maybe a) :: Maybe b where
LiftMaybe f Nothing = Nothing
LiftMaybe f (Just a) = Just (Apply f a)
#if __GLASGOW_HASKELL__ >= 810
type LiftMaybeSym0 :: forall a b. (a ~> b) ~> Maybe a ~> Maybe b
type LiftMaybeSym1 :: forall a b. (a ~> b) -> Maybe a ~> Maybe b
#endif
data LiftMaybeSym0 :: forall a b. (a ~> b) ~> Maybe a ~> Maybe b
data LiftMaybeSym1 :: forall a b. (a ~> b) -> Maybe a ~> Maybe b
type instance Apply LiftMaybeSym0 k1 = LiftMaybeSym1 k1
type instance Apply (LiftMaybeSym1 k1) k2 = LiftMaybe k1 k2
sLiftMaybe :: forall a b (f :: a ~> b) (x :: Maybe a).
(forall (y :: a). Proxy f -> Sing y -> Sing (Apply f y)) ->
Sing x -> Sing (LiftMaybe f x)
sLiftMaybe _ SNothing = SNothing
sLiftMaybe f (SJust a) = SJust (f Proxy a)
(+) :: Nat -> Nat -> Nat
Zero + x = x
(Succ x) + y = Succ (x + y)
#if __GLASGOW_HASKELL__ >= 810
type (+) :: Nat -> Nat -> Nat
#endif
type family (+) (m :: Nat) (n :: Nat) :: Nat where
Zero + x = x
(Succ x) + y = Succ (x + y)
-- defunctionalization symbols
#if __GLASGOW_HASKELL__ >= 810
type (+@#@$) :: Nat ~> Nat ~> Nat
type (+@#@$$) :: Nat -> Nat ~> Nat
#endif
data (+@#@$) :: Nat ~> Nat ~> Nat
data (+@#@$$) :: Nat -> Nat ~> Nat
type instance Apply (+@#@$) k1 = (+@#@$$) k1
type instance Apply ((+@#@$$) k1) k2 = (+) k1 k2
(%+) :: Sing m -> Sing n -> Sing (m + n)
SZero %+ x = x
(SSucc x) %+ y = SSucc (x %+ y)
(-) :: Nat -> Nat -> Nat
Zero - _ = Zero
(Succ x) - Zero = Succ x
(Succ x) - (Succ y) = x - y
#if __GLASGOW_HASKELL__ >= 810
type (-) :: Nat -> Nat -> Nat
#endif
type family (-) (m :: Nat) (n :: Nat) :: Nat where
Zero - x = Zero
(Succ x) - Zero = Succ x
(Succ x) - (Succ y) = x - y
#if __GLASGOW_HASKELL__ >= 810
type (-@#@$) :: Nat ~> Nat ~> Nat
type (-@#@$$) :: Nat -> Nat ~> Nat
#endif
data (-@#@$) :: Nat ~> Nat ~> Nat
data (-@#@$$) :: Nat -> Nat ~> Nat
type instance Apply (-@#@$) k1 = (-@#@$$) k1
type instance Apply ((-@#@$$) k1) k2 = (-) k1 k2
(%-) :: Sing m -> Sing n -> Sing (m - n)
SZero %- _ = SZero
(SSucc x) %- SZero = SSucc x
(SSucc x) %- (SSucc y) = x %- y
isZero :: Nat -> Bool
isZero n = if n == Zero then True else False
#if __GLASGOW_HASKELL__ >= 810
type IsZero :: Nat -> Bool
#endif
type family IsZero (n :: Nat) :: Bool where
IsZero n = If (n == Zero) True False
#if __GLASGOW_HASKELL__ >= 810
type IsZeroSym0 :: Nat ~> Bool
#endif
data IsZeroSym0 :: Nat ~> Bool
type instance Apply IsZeroSym0 a = IsZero a
sIsZero :: Sing n -> Sing (IsZero n)
sIsZero n = sIf (n %== SZero) STrue SFalse
{-
(||) :: Bool -> Bool -> Bool
False || x = x
True || _ = True
-}
#if __GLASGOW_HASKELL__ >= 810
type (||) :: Bool -> Bool -> Bool
#endif
type family (a :: Bool) || (b :: Bool) :: Bool where
False || x = x
True || x = True
#if __GLASGOW_HASKELL__ >= 810
type (||@#@$) :: Bool ~> Bool ~> Bool
type (||@#@$$) :: Bool -> Bool ~> Bool
#endif
data (||@#@$) :: Bool ~> Bool ~> Bool
data (||@#@$$) :: Bool -> Bool ~> Bool
type instance Apply (||@#@$) a = (||@#@$$) a
type instance Apply ((||@#@$$) a) b = (||) a b
(%||) :: Sing a -> Sing b -> Sing (a || b)
SFalse %|| x = x
STrue %|| _ = STrue
contains :: Eq a => a -> List a -> Bool
contains _ Nil = False
contains elt (Cons h t) = (elt == h) || contains elt t
#if __GLASGOW_HASKELL__ >= 810
type Contains :: k -> List k -> Bool
#endif
type family Contains (a :: k) (b :: List k) :: Bool where
Contains elt Nil = False
Contains elt (Cons h t) = (elt == h) || (Contains elt t)
#if __GLASGOW_HASKELL__ >= 810
type ContainsSym0 :: forall a. a ~> List a ~> Bool
type ContainsSym1 :: forall a. a -> List a ~> Bool
#endif
data ContainsSym0 :: forall a. a ~> List a ~> Bool
data ContainsSym1 :: forall a. a -> List a ~> Bool
type instance Apply ContainsSym0 a = ContainsSym1 a
type instance Apply (ContainsSym1 a) b = Contains a b
{-
sContains :: forall k. SEq k =>
forall (a :: k). Sing a ->
forall (list :: List k). Sing list -> Sing (Contains a list)
sContains _ SNil = SFalse
sContains elt (SCons h t) = (elt %== h) %|| (sContains elt t)
-}
sContains :: forall a (t1 :: a) (t2 :: List a). SEq a => Sing t1
-> Sing t2 -> Sing (Contains t1 t2)
sContains _ SNil =
let lambda :: forall wild. Sing (Contains wild Nil)
lambda = SFalse
in
lambda
sContains elt (SCons h t) =
let lambda :: forall elt h t. (elt ~ t1, (Cons h t) ~ t2) => Sing elt -> Sing h -> Sing t -> Sing (Contains elt (Cons h t))
lambda elt' h' t' = (elt' %== h') %|| sContains elt' t'
in
lambda elt h t
cont :: Eq a => a -> List a -> Bool
cont = \elt list -> case list of
Nil -> False
Cons h t -> (elt == h) || cont elt t
#if __GLASGOW_HASKELL__ >= 810
type Cont :: a ~> List a ~> Bool
#endif
type family Cont :: a ~> List a ~> Bool where
Cont = Lambda10Sym0
data Lambda10Sym0 f where
KindInferenceLambda10Sym0 :: (Lambda10Sym0 @@ arg) ~ Lambda10Sym1 arg
=> Proxy arg
-> Lambda10Sym0 f
type instance Lambda10Sym0 `Apply` x = Lambda10Sym1 x
data Lambda10Sym1 a f where
KindInferenceLambda10Sym1 :: (Lambda10Sym1 a @@ arg) ~ Lambda10Sym2 a arg
=> Proxy arg
-> Lambda10Sym1 a f
type instance (Lambda10Sym1 a) `Apply` b = Lambda10Sym2 a b
type Lambda10Sym2 a b = Lambda10 a b
type family Lambda10 a b where
Lambda10 elt list = Case10 elt list list
type family Case10 a b scrut where
Case10 elt list Nil = False
Case10 elt list (Cons h t) = (||@#@$) @@ ((==@#@$) @@ elt @@ h) @@ (Cont @@ elt @@ t)
data (==@#@$) f where
(:###==@#@$) :: ((==@#@$) @@ arg) ~ (==@#@$$) arg
=> Proxy arg
-> (==@#@$) f
type instance (==@#@$) `Apply` x = (==@#@$$) x
data (==@#@$$) a f where
(:###==@#@$$) :: ((==@#@$$) x @@ arg) ~ (==@#@$$$) x arg
=> Proxy arg
-> (==@#@$$) x y
type instance (==@#@$$) a `Apply` b = (==) a b
type family (==@#@$$$) a b where
(==@#@$$$) a b = (==) a b
impNat :: forall m n. SingI n => Proxy n -> Sing m -> Sing (n + m)
impNat _ sm = (sing :: Sing n) %+ sm
callImpNat :: forall n m. Sing n -> Sing m -> Sing (n + m)
callImpNat sn sm = withSingI sn (impNat (Proxy :: Proxy n) sm)
instance Show (SNat n) where
show SZero = "SZero"
show (SSucc n) = "SSucc (" ++ (show n) ++ ")"
findIndices :: (a -> Bool) -> [a] -> [Nat]
findIndices p ls = loop Zero ls
where
loop _ [] = []
loop n (x:xs) | p x = n : loop (Succ n) xs
| otherwise = loop (Succ n) xs
#if __GLASGOW_HASKELL__ >= 810
type FindIndices :: (a ~> Bool) -> List a -> List Nat
#endif
type family FindIndices (f :: a ~> Bool) (ls :: List a) :: List Nat where
FindIndices p ls = (Let123LoopSym2 p ls) @@ Zero @@ ls
type family Let123Loop p ls (arg1 :: Nat) (arg2 :: List a) :: List Nat where
Let123Loop p ls z Nil = Nil
Let123Loop p ls n (x `Cons` xs) = Case123 p ls n x xs (p @@ x)
type family Case123 p ls n x xs scrut where
Case123 p ls n x xs True = n `Cons` ((Let123LoopSym2 p ls) @@ (Succ n) @@ xs)
Case123 p ls n x xs False = (Let123LoopSym2 p ls) @@ (Succ n) @@ xs
data Let123LoopSym2 a b c where
Let123LoopSym2KindInfernece :: ((Let123LoopSym2 a b @@ z) ~ Let123LoopSym3 a b z)
=> Proxy z
-> Let123LoopSym2 a b c
type instance Apply (Let123LoopSym2 a b) c = Let123LoopSym3 a b c
data Let123LoopSym3 a b c d where
KindInferenceLet123LoopSym3 :: ((Let123LoopSym3 a b c @@ z) ~ Let123LoopSym4 a b c z)
=> Proxy z
-> Let123LoopSym3 a b c d
type instance Apply (Let123LoopSym3 a b c) d = Let123Loop a b c d
type family Let123LoopSym4 a b c d where
Let123LoopSym4 a b c d = Let123Loop a b c d
data FindIndicesSym0 a where
KindInferenceFindIndicesSym0 :: (FindIndicesSym0 @@ z) ~ FindIndicesSym1 z
=> Proxy z
-> FindIndicesSym0 a
type instance Apply FindIndicesSym0 a = FindIndicesSym1 a
data FindIndicesSym1 a b where
KindInferenceFindIndicesSym1 :: (FindIndicesSym1 a @@ z) ~ FindIndicesSym2 a z
=> Proxy z
-> FindIndicesSym1 a b
type instance Apply (FindIndicesSym1 a) b = FindIndices a b
type family FindIndicesSym2 a b where
FindIndicesSym2 a b = FindIndices a b
sFindIndices :: forall a (t1 :: a ~> Bool) (t2 :: (List a)).
Sing t1
-> Sing t2
-> Sing (FindIndicesSym0 @@ t1 @@ t2)
sFindIndices sP sLs =
let sLoop :: forall (u1 :: Nat) (u2 :: List a).
Sing u1 -> Sing u2
-> Sing ((Let123LoopSym2 t1 t2) @@ u1 @@ u2)
sLoop _ SNil = SNil
sLoop sN (sX `SCons` sXs) = case sP @@ sX of
STrue -> (singFun2 @ConsSym0 SCons) @@ sN @@
((singFun2 @(Let123LoopSym2 t1 t2) sLoop) @@ ((singFun1 @SuccSym0 SSucc) @@ sN) @@ sXs)
SFalse -> (singFun2 @(Let123LoopSym2 t1 t2) sLoop) @@ ((singFun1 @SuccSym0 SSucc) @@ sN) @@ sXs
in
(singFun2 @(Let123LoopSym2 t1 t2) sLoop) @@ SZero @@ sLs
fI :: forall a. (a -> Bool) -> [a] -> [Nat]
fI = \p ls ->
let loop :: Nat -> [a] -> [Nat]
loop _ [] = []
loop n (x:xs) = case p x of
True -> n : loop (Succ n) xs
False -> loop (Succ n) xs
in
loop Zero ls
type FI = Lambda22Sym0
type FISym0 = FI
type family Lambda22 p ls where
Lambda22 p ls = (Let123LoopSym2 p ls) @@ Zero @@ ls
data Lambda22Sym0 a where
KindInferenceLambda22Sym0 :: (Lambda22Sym0 @@ z) ~ Lambda22Sym1 z
=> Proxy z
-> Lambda22Sym0 a
type instance Apply Lambda22Sym0 a = Lambda22Sym1 a
data Lambda22Sym1 a b where
KindInferenceLambda22Sym1 :: (Lambda22Sym1 a @@ z) ~ Lambda22Sym2 a z
=> Proxy z
-> Lambda22Sym1 a b
type instance Apply (Lambda22Sym1 a) b = Lambda22 a b
type family Lambda22Sym2 a b where
Lambda22Sym2 a b = Lambda22 a b
{-
sFI :: forall a (t1 :: a ~> Bool) (t2 :: List a). Sing t1
-> Sing t2
-> Sing (FISym0 @@ t1 @@ t2)
sFI = unSingFun2 (singFun2 @FI (\p ls ->
let lambda :: forall {-(t1 :: a ~> Bool)-} t1 t2. Sing t1 -> Sing t2 -> Sing (Lambda22Sym0 @@ t1 @@ t2)
lambda sP sLs =
let sLoop :: (Lambda22Sym0 @@ t1 @@ t2) ~ (Let123LoopSym2 t1 t2 @@ Zero @@ t2) => forall (u1 :: Nat). Sing u1
-> forall {-(u2 :: List a)-} u2. Sing u2
-> Sing ((Let123LoopSym2 t1 t2) @@ u1 @@ u2)
sLoop _ SNil = SNil
sLoop sN (sX `SCons` sXs) = case sP @@ sX of
STrue -> (singFun2 @ConsSym0 SCons) @@ sN @@
((singFun2 @(Let123LoopSym2 t1 t2) sLoop) @@ ((singFun1 @SuccSym0 SSucc) @@ sN) @@ sXs)
SFalse -> (singFun2 @(Let123LoopSym2 t1 t2) sLoop) @@ ((singFun1 @SuccSym0 SSucc) @@ sN) @@ sXs
in
(singFun2 @(Let123LoopSym2 t1 t2) sLoop) @@ SZero @@ sLs
in
lambda p ls
))
-}
------------------------------------------------------------
#if __GLASGOW_HASKELL__ >= 810
type G :: Type -> Type
#endif
data G :: Type -> Type where
MkG :: G Bool
#if __GLASGOW_HASKELL__ >= 810
type SG :: forall a. G a -> Type
#endif
data SG :: forall a. G a -> Type where
SMkG :: SG MkG
type instance Sing = SG