eliminators 0.2 → 0.3

raw patch · 12 files changed

+615/−266 lines, 12 filesdep +singleton-natsPVP ok

version bump matches the API change (PVP)

Dependencies added: singleton-nats

API changes (from Hackage documentation)

Files

• CHANGELOG.md +7/−0
• eliminators.cabal +17/−13
• src/Data/Eliminator.hs +8/−28
• src/Data/Eliminator/TH.hs +1/−1
• src/Data/Eliminator/TypeNats.hs +39/−0
• tests/DecideSpec.hs +222/−0
• tests/DecideTypes.hs +106/−0
• tests/EqualitySpec.hs +30/−8
• tests/PeanoSpec.hs +0/−117
• tests/PeanoTypes.hs +0/−94
• tests/VecSpec.hs +105/−5
• tests/VecTypes.hs +80/−0

@@ -1,3 +1,10 @@+## 0.3 [2017-11-07]+* Migrate the old `elimNat` from `Data.Eliminator` (which worked over the `Nat`+  from `GHC.TypeNats`) to `Data.Eliminator.TypeNats`. There `elimNat` that now+  lives in `Data.Eliminator` is for an unrelated `Nat` data type from the+  `singleton-nats` package (which is a proper, inductively defined, Peano+  natural number type).+ ## 0.2 [2017-07-22] * Introduce the `Data.Eliminator.TH` module, which provides functionality for   generating eliminator functions using Template Haskell. Currently, only

@@ -1,5 +1,5 @@ name:                eliminators-version:             0.2+version:             0.3 synopsis:            Dependently typed elimination functions using singletons description:         This library provides eliminators for inductive data types,                      leveraging the power of the @singletons@ library to allow@@ -25,12 +25,14 @@ library   exposed-modules:     Data.Eliminator                        Data.Eliminator.TH-  build-depends:       base             >= 4.10  && < 4.11-                     , extra            >= 1.4.2 && < 1.7-                     , singletons       >= 2.3   && < 2.4-                     , template-haskell >= 2.12  && < 2.13-                     , th-abstraction   >= 0.2.3 && < 0.3-                     , th-desugar       >= 1.7   && < 1.8+                       Data.Eliminator.TypeNats+  build-depends:       base             >= 4.10    && < 4.11+                     , extra            >= 1.4.2   && < 1.7+                     , singletons       >= 2.3     && < 2.4+                     , singleton-nats   >= 0.4.0.3 && < 0.5+                     , template-haskell >= 2.12    && < 2.13+                     , th-abstraction   >= 0.2.3   && < 0.3+                     , th-desugar       >= 1.7     && < 1.8   hs-source-dirs:      src   default-language:    Haskell2010   ghc-options:         -Wall -Wno-unticked-promoted-constructors@@ -38,17 +40,19 @@ test-suite spec   type:                exitcode-stdio-1.0   main-is:             Spec.hs-  other-modules:       EqualitySpec+  other-modules:       DecideSpec+                       DecideTypes+                       EqualitySpec                        GADTSpec                        ListSpec                        ListTypes-                       PeanoSpec-                       PeanoTypes+                       VecTypes                        VecSpec-  build-depends:       base       >= 4.10 && < 4.11+  build-depends:       base           >= 4.10    && < 4.11                      , eliminators-                     , hspec      >= 2    && < 3-                     , singletons >= 2.3  && < 2.4+                     , hspec          >= 2       && < 3+                     , singletons     >= 2.3     && < 2.4+                     , singleton-nats >= 0.4.0.3 && < 0.5   hs-source-dirs:      tests   default-language:    Haskell2010   ghc-options:         -Wall -Wno-unticked-promoted-constructors -threaded -rtsopts

@@ -39,20 +39,15 @@   , elimTuple7   ) where -import           Control.Monad.Extra--import           Data.Eliminator.TH-import           Data.Kind (Type)-import           Data.List.NonEmpty (NonEmpty(..))-import           Data.Singletons.Prelude-import           Data.Singletons.Prelude.List.NonEmpty (Sing(..))-import           Data.Singletons.TypeLits--import qualified GHC.TypeLits as TL+import Control.Monad.Extra -import           Language.Haskell.TH.Desugar (tupleNameDegree_maybe)+import Data.Eliminator.TH+import Data.List.NonEmpty (NonEmpty(..))+import Data.Nat+import Data.Singletons.Prelude+import Data.Singletons.Prelude.List.NonEmpty (Sing(..)) -import           Unsafe.Coerce (unsafeCoerce)+import Language.Haskell.TH.Desugar (tupleNameDegree_maybe)  {- $eliminators @@ -70,23 +65,8 @@   with @~>@ prepended. -} -$(concatMapM deriveElim [''Bool, ''Either, ''Maybe, ''NonEmpty, ''Ordering])+$(concatMapM deriveElim [''Bool, ''Either, ''Maybe, ''Nat, ''NonEmpty, ''Ordering]) $(deriveElimNamed "elimList" ''[]) $(concatMapM (\n -> let Just deg = tupleNameDegree_maybe n                     in deriveElimNamed ("elimTuple" ++ show deg) n)              [''(), ''(,), ''(,,), ''(,,,), ''(,,,,), ''(,,,,,), ''(,,,,,,)])---- This is the grimy one we can't define using Template Haskell.---- | Although 'Nat' is not actually an inductive data type in GHC, we can--- pretend that it is using this eliminator.-elimNat :: forall (p :: Nat ~> Type) (n :: Nat).-           Sing n-        -> p @@ 0-        -> (forall (k :: Nat). Sing k -> p @@ k -> p @@ (k TL.+ 1))-        -> p @@ n-elimNat snat pZ pS =-  case fromSing snat of-    0        -> unsafeCoerce pZ-    nPlusOne -> withSomeSing (pred nPlusOne) $ \(sn :: Sing k) ->-                  unsafeCoerce (pS sn (elimNat @p @k sn pZ pS))

@@ -53,7 +53,7 @@            -> p '@@' l elimMyList SMyNil pMyNil _ = pMyNil elimMyList (SMyCons (x' :: 'Sing' x) (xs' :: 'Sing' xs)) pMyNil pMyCons-  = pMyCons x' xs' (elimMyList @a @p @xs pMyNil pMyCons)+  = pMyCons x' xs' (elimMyList \@a \@p \@xs pMyNil pMyCons) @  There are some important things to note here:

@@ -0,0 +1,39 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-|+Module:      Data.Eliminator.TypeNats+Copyright:   (C) 2017 Ryan Scott+License:     BSD-style (see the file LICENSE)+Maintainer:  Ryan Scott+Stability:   Experimental+Portability: GHC++A crude imitation of an eliminator function for 'GHC.TypeNats.Nat'.+-}+module Data.Eliminator.TypeNats (elimNat) where++import Data.Kind (Type)+import Data.Singletons+import Data.Singletons.TypeLits++import GHC.TypeNats++import Unsafe.Coerce (unsafeCoerce)++-- | Although 'Nat' is not actually an inductive data type in GHC, we can+-- (crudely) pretend that it is using this eliminator.+elimNat :: forall (p :: Nat ~> Type) (n :: Nat).+           Sing n+        -> p @@ 0+        -> (forall (k :: Nat). Sing k -> p @@ k -> p @@ (k + 1))+        -> p @@ n+elimNat snat pZ pS =+  case fromSing snat of+    0        -> unsafeCoerce pZ+    nPlusOne -> withSomeSing (pred nPlusOne) $ \(sn :: Sing k) ->+                  unsafeCoerce (pS sn (elimNat @p @k sn pZ pS))

@@ -0,0 +1,222 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+module DecideSpec where++import Data.Eliminator+import Data.Nat+import Data.Singletons.Prelude+import Data.Singletons.TH hiding (Decision(..))+import Data.Type.Equality++import EqualitySpec (cong, replace)+import DecideTypes++import Test.Hspec++main :: IO ()+main = hspec spec++spec :: Spec+spec = parallel $ do+  let proved    = "Proved Refl"+      disproved = "Disproved <void>"+  describe "decEqNat" $ do+    it "returns evidence that two Nats are equal" $ do+      show (decEqNat (sLit @0) (sLit @0)) `shouldBe` proved+      show (decEqNat (sLit @1) (sLit @0)) `shouldBe` disproved+      show (decEqNat (sLit @0) (sLit @1)) `shouldBe` disproved+      show (decEqNat (sLit @1) (sLit @1)) `shouldBe` proved+  describe "decEqList" $ do+    it "returns evidence that two lists are equal" $ do+      let decEqNatList = decEqList decEqNat+      show (decEqNatList SNil                   SNil)                   `shouldBe` proved+      show (decEqNatList (SCons (sLit @0) SNil) SNil)                   `shouldBe` disproved+      show (decEqNatList SNil                   (SCons (sLit @0) SNil)) `shouldBe` disproved+      show (decEqNatList (SCons (sLit @0) SNil) (SCons (sLit @0) SNil)) `shouldBe` proved+      -- TODO: Try this in the next version of singletons+      -- show (decEqNatList (SCons (sLit @1) SNil) (SCons (sLit @0) SNil)) `shouldBe` disproved++-----++peanoEqConsequencesSame :: forall (n :: Nat). Sing n -> NatEqConsequences n n+peanoEqConsequencesSame sn = elimNat @WhyNatEqConsequencesSameSym0 @n sn base step+  where+    base :: WhyNatEqConsequencesSame Z+    base = ()++    step :: forall (k :: Nat).+            Sing k+         -> WhyNatEqConsequencesSame k+         -> WhyNatEqConsequencesSame (S k)+    step _ _ = Refl++useNatEq :: forall n j. Sing n -> n :~: j -> NatEqConsequences n j+useNatEq sn nEqJ = replace @Nat @n @j @(NatEqConsequencesSym1 n)+                             (peanoEqConsequencesSame @n sn) nEqJ++zNotS :: forall n. Z :~: S n -> Void+zNotS = useNatEq @Z @(S n) SZ++sNotZ :: forall n. S n :~: Z -> Void+sNotZ eq = zNotS @n (sym eq)++sInjective :: forall n j. Sing n -> S n :~: S j -> n :~: j+sInjective sn = useNatEq @(S n) @(S j) (SS sn)++decEqZ :: forall (j :: Nat). Sing j -> Decision (Z :~: j)+decEqZ sj = elimNat @WhyDecEqZSym0 @j sj base step+  where+    base :: Decision (Z :~: Z)+    base = Proved Refl++    step :: forall (k :: Nat).+            Sing k -> Decision (Z :~: k) -> Decision (Z :~: S k)+    step _ _ = Disproved (zNotS @k)++decCongS :: forall n j. Sing n -> Decision (n :~: j) -> Decision (S n :~: S j)+decCongS sn dNJ = withSomeSing dNJ $ \(sDNJ :: Sing d) ->+                    elimDecision @_ @(ConstSym1 (Decision (S n :~: S j))) @d+                      sDNJ left right+  where+    left :: forall (x :: n :~: j).+            Sing x -> Decision (S n :~: S j)+    left yes = Proved $ cong @Nat @Nat @(TyCon1 S) @n @j (fromSing yes)++    right :: forall (r :: (n :~: j) ~> Void).+             Sing r -> Decision (S n :~: S j)+    right no = Disproved $ fromSing no . sInjective @n @j sn++decEqNat :: forall (n :: Nat) (j :: Nat). Sing n -> Sing j -> Decision (n :~: j)+decEqNat sn = runWhyDecEqNat (elimNat @(TyCon1 WhyDecEqNat) @n sn base step)+  where+    base :: WhyDecEqNat Z+    base = WhyDecEqNat decEqZ++    step :: forall (k :: Nat).+            Sing k+         -> WhyDecEqNat k+         -> WhyDecEqNat (S k)+    step sk swhyK = WhyDecEqNat $ \(sl :: Sing l) ->+                      elimNat @(WhyDecEqSSym1 k) @l sl baseStep stepStep+      where+        baseStep :: Decision (S k :~: Z)+        baseStep = Disproved $ sNotZ @k++        stepStep :: forall (m :: Nat).+                    Sing m+                 -> Decision (S k :~: m)+                 -> Decision (S k :~: S m)+        stepStep sm _ = decCongS sk (runWhyDecEqNat swhyK sm)++listEqConsequencesSame :: forall (es :: [e]). Sing es -> ListEqConsequences es es+listEqConsequencesSame sl = elimList @e @WhyListEqConsequencesSameSym0 @es sl base step+  where+    base :: ListEqConsequences '[] '[]+    base = ()++    step :: forall (x :: e) (xs :: [e]).+            Sing x -> Sing xs+         -> ListEqConsequences xs xs+         -> ListEqConsequences (x:xs) (x:xs)+    step _ _ _ = (Refl, Refl)++useListEq :: forall (xs :: [e]) (ys :: [e]).+             Sing xs -> xs :~: ys -> ListEqConsequences xs ys+useListEq sxs xsEqYs = replace @[e] @xs @ys @(ListEqConsequencesSym1 xs)+                               (listEqConsequencesSame @e @xs sxs) xsEqYs++nilNotCons :: forall (x :: e) (xs :: [e]). '[] :~: (x:xs) -> Void+nilNotCons = useListEq @e @'[] @(x:xs) SNil++consNotNil :: forall (x :: e) (xs :: [e]). (x:xs) :~: '[] -> Void+consNotNil eq = nilNotCons @e @x @xs (sym eq)++consInjective :: forall (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).+                 Sing x -> Sing xs+              -> (x:xs) :~: (y:ys)+              -> (x :~: y, xs :~: ys)+consInjective sx sxs = useListEq @e @(x:xs) @(y:ys) (SCons sx sxs)++decEqNil :: forall (es :: [e]). Sing es -> Decision ('[] :~: es)+decEqNil ses = elimList @e @WhyDecEqNilSym0 @es ses base step+  where+    base :: Decision ('[] :~: '[])+    base = Proved Refl++    step :: forall (x :: e) (xs :: [e]).+            Sing x -> Sing xs+         -> Decision ('[] :~: xs)+         -> Decision ('[] :~: (x:xs))+    step _ _ _ = Disproved (nilNotCons @e @x @xs)++intermixListEqs :: forall (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).+                   x :~: y -> xs :~: ys+                -> (x:xs) :~: (y:ys)+intermixListEqs xEqY xsEqYs =+  replace @e @x @y @(WhyIntermixListEqs1Sym3 x xs ys)+          (replace @[e] @xs @ys @(WhyIntermixListEqs2Sym2 x xs) Refl xsEqYs)+          xEqY++decCongCons :: forall (x :: e) (xs :: [e]) (y :: e) (ys :: [e]).+               Sing x -> Sing xs+            -> Decision (x :~: y) -> Decision (xs :~: ys)+            -> Decision ((x:xs) :~: (y:ys))+decCongCons sx sxs dXY dXsYs =+  withSomeSing dXY $ \(sDXY :: Sing dXY) ->+    elimDecision @_ @(ConstSym1 (Decision ((x:xs) :~: (y:ys)))) @dXY+      sDXY left right+  where+    left :: forall (z :: x :~: y).+            Sing z -> Decision ((x:xs) :~: (y:ys))+    left xEqY = withSomeSing dXsYs $ \(sDXsYs :: Sing dXsYs) ->+                  elimDecision @_ @(ConstSym1 (Decision ((x:xs) :~: (y:ys)))) @dXsYs+                    sDXsYs leftLeft leftRight+      where+        leftLeft :: forall (zz :: xs :~: ys).+                    Sing zz -> Decision ((x:xs) :~: (y:ys))+        leftLeft xsEqYs = Proved $ intermixListEqs (fromSing xEqY) (fromSing xsEqYs)++        leftRight :: forall (r :: (xs :~: ys) ~> Void).+                     Sing r -> Decision ((x:xs) :~: (y:ys))+        leftRight no = Disproved $ fromSing no . snd . injective++    right :: forall (r :: (x :~: y) ~> Void).+             Sing r -> Decision ((x:xs) :~: (y:ys))+    right no = Disproved $ fromSing no . fst . injective++    injective :: (x:xs) :~: (y:ys) -> (x :~: y, xs :~: ys)+    injective = consInjective @e @x @xs @y @ys sx sxs++decEqList :: forall (es1 :: [e]) (es2 :: [e]).+             (forall (e1 :: e) (e2 :: e).+                     Sing e1 -> Sing e2 -> Decision (e1 :~: e2))+          -> Sing es1 -> Sing es2 -> Decision (es1 :~: es2)+decEqList f ses1 = runWhyDecEqList (elimList @e @(TyCon1 WhyDecEqList) @es1 ses1 base step)+  where+    base :: WhyDecEqList '[]+    base = WhyDecEqList decEqNil++    step :: forall (x :: e) (xs :: [e]).+            Sing x -> Sing xs+         -> WhyDecEqList xs+         -> WhyDecEqList (x:xs)+    step sx sxs swhyXs = WhyDecEqList $ \(sl :: Sing l) ->+                           elimList @e @(WhyDecEqConsSym2 x xs) @l sl+                             stepBase stepStep+      where+        stepBase :: Decision ((x:xs) :~: '[])+        stepBase = Disproved $ consNotNil @e @x @xs++        stepStep :: forall (y :: e) (ys :: [e]).+                    Sing y -> Sing ys+                 -> Decision ((x:xs) :~: ys)+                 -> Decision ((x:xs) :~: (y:ys))+        stepStep sy sys _ = decCongCons sx sxs+                                        (f sx sy)+                                        (runWhyDecEqList swhyXs sys)

@@ -0,0 +1,106 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+-- TODO: Remove this in the next version of singletons+{-# OPTIONS_GHC -Wno-orphans #-}+module DecideTypes where++import Data.Kind+import Data.Nat+import Data.Singletons.TH hiding (Decision(..))++-- TODO: Remove these in the next version of singletons+$(genSingletons [''Void])+$(genDefunSymbols [''(~>)])++-- Due to https://github.com/goldfirere/singletons/issues/82, promoting the+-- Decision data type from Data.Singletons.Decide is a tad awkward. To work+-- around these, we define a more general Decision' data type here.+data Decision' p a+  = Proved a+  | Disproved (p @@ a @@ Void)++elimDecision :: forall (a :: Type) (p :: PDecision a ~> Type) (d :: PDecision a).+                Sing d+             -> (forall (yes :: a). Sing yes -> p @@ (Proved yes))+             -> (forall (no :: a ~> Void). Sing no -> p @@ (Disproved no))+             -> p @@ d+elimDecision (SProved yes)   pProved _          = pProved yes+elimDecision (SDisproved no) _       pDisproved = pDisproved no++instance Show a => Show (Decision' p a) where+  showsPrec p (Proved a) =+    showParen (p > 10) $ showString "Proved " . showsPrec 11 a+  showsPrec p (Disproved _) =+    showParen (p > 10) $ showString "Disproved <void>"++type Decision  = Decision' (TyCon2 (->))+type PDecision = Decision' (:~>$)++data instance Sing (z :: PDecision a) where+  -- It would be lovely to not have to write those (:: PDecision a) kind+  -- ascriptions in the return types of each constructor.+  -- See https://ghc.haskell.org/trac/ghc/ticket/14111.+  SProved    :: forall (x :: a).         Sing x -> Sing (Proved x    :: PDecision a)+  SDisproved :: forall (r :: a ~> Void). Sing r -> Sing (Disproved r :: PDecision a)++instance SingKind a => SingKind (PDecision a) where+  type Demote (PDecision a) = Decision (Demote a)+  fromSing (SProved a)    = Proved (fromSing a)+  fromSing (SDisproved r) = Disproved (fromSing r)+  toSing (Proved x)    = withSomeSing x $ SomeSing . SProved+  toSing (Disproved r) = withSomeSing r $ SomeSing . SDisproved++type family NatEqConsequences (a :: Nat) (b :: Nat) :: Type where+  NatEqConsequences Z      Z      = ()+  NatEqConsequences Z      (S _)  = Void+  NatEqConsequences (S _)  Z      = Void+  NatEqConsequences (S k1) (S k2) = k1 :~: k2+$(genDefunSymbols [''NatEqConsequences])++type WhyNatEqConsequencesSame (a :: Nat) = NatEqConsequences a a+$(genDefunSymbols [''WhyNatEqConsequencesSame])++type WhyDecEqZ (k :: Nat) = Decision (Z :~: k)+$(genDefunSymbols [''WhyDecEqZ])++type WhyDecEqS (n :: Nat) (k :: Nat) = Decision (S n :~: k)+$(genDefunSymbols [''WhyDecEqS])++-- The newtype wrapper is needed to work around+-- https://github.com/goldfirere/singletons/issues/198+newtype WhyDecEqNat (k :: Nat) = WhyDecEqNat+  { runWhyDecEqNat :: forall (j :: Nat). Sing j -> Decision (k :~: j) }++type family ListEqConsequences (xxs :: [e]) (yys :: [e]) :: Type where+  ListEqConsequences '[]    '[]    = ()+  ListEqConsequences '[]    (_:_)  = Void+  ListEqConsequences (_:_)  '[]    = Void+  ListEqConsequences (x:xs) (y:ys) = (x :~: y, xs :~: ys)+$(genDefunSymbols [''ListEqConsequences])++type WhyListEqConsequencesSame (es :: [e]) = ListEqConsequences es es+$(genDefunSymbols [''WhyListEqConsequencesSame])++type WhyDecEqNil (es :: [e]) = Decision ('[] :~: es)+$(genDefunSymbols [''WhyDecEqNil])++type WhyDecEqCons (x :: e) (xs :: [e]) (es :: [e]) = Decision ((x:xs) :~: es)+$(genDefunSymbols [''WhyDecEqCons])++type WhyIntermixListEqs1 (x :: e) (xs :: [e]) (ys :: [e]) (k :: e) = (x:xs) :~: (k:ys)+type WhyIntermixListEqs2 (x :: e) (xs :: [e]) (k :: [e])           = (x:xs) :~: (x:k)+$(genDefunSymbols [''WhyIntermixListEqs1, ''WhyIntermixListEqs2])++-- The newtype wrapper is needed to work around+-- https://github.com/goldfirere/singletons/issues/198+newtype WhyDecEqList (l1 :: [e]) = WhyDecEqList+  { runWhyDecEqList :: forall (l2 :: [e]). Sing l2 -> Decision (l1 :~: l2) }

@@ -43,7 +43,9 @@ instance SingI Refl where   sing = SRefl -(~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).+(~>:~:) :: forall (k :: Type) (a :: k) (b :: k)+                  (p :: forall (y :: k). a :~: y ~> Type)+                  (r :: a :~: b).            Sing r         -> p @@ Refl         -> p @@ r@@ -61,7 +63,9 @@ instance SingI HRefl where   sing = SHRefl -(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y ~> Type).+(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)+                   (p :: forall (z :: Type) (y :: z). a :~~: y ~> Type)+                   (r :: a :~~: b).             Sing r          -> p @@ HRefl          -> p @@ r@@ -77,7 +81,7 @@ sym :: forall (t :: Type) (a :: t) (b :: t).        a :~: b -> b :~: a sym eq = withSomeSing eq $ \(singEq :: Sing r) ->-           (~>:~:) @t @a @b @r @(WhySymSym a) singEq Refl+           (~>:~:) @t @a @b @(WhySymSym a) @r singEq Refl  type WhyHsym (a :: j) (y :: z) (e :: a :~~: y) = y :~~: a data WhyHsymSym (a :: j) :: forall (z :: Type) (y :: z). a :~~: y ~> Type@@ -87,7 +91,7 @@ hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).         a :~~: b -> b :~~: a hsym eq = withSomeSing eq $ \(singEq :: Sing r) ->-            (~>:~~:) @j @k @a @b @r @(WhyHsymSym a) singEq HRefl+            (~>:~~:) @j @k @a @b @(WhyHsymSym a) @r singEq HRefl  type family Symmetry (x :: (a :: k) :~: (b :: k)) :: b :~: a where   Symmetry Refl = Refl@@ -101,7 +105,7 @@ symIdempotent :: forall (t :: Type) (a :: t) (b :: t)                         (e :: a :~: b).                  Sing e -> Symmetry (Symmetry e) :~: e-symIdempotent se = (~>:~:) @t @a @b @e @(WhySymIdempotentSym a) se Refl+symIdempotent se = (~>:~:) @t @a @b @(WhySymIdempotentSym a) @e se Refl  type family Hsymmetry (x :: (a :: j) :~~: (b :: k)) :: b :~~: a where   Hsymmetry HRefl = HRefl@@ -115,7 +119,7 @@ hsymIdempotent :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)                          (e :: a :~~: b).                   Sing e -> Hsymmetry (Hsymmetry e) :~: e-hsymIdempotent se = (~>:~~:) @j @k @a @b @e @(WhyHsymIdempotentSym a) se Refl+hsymIdempotent se = (~>:~~:) @j @k @a @b @(WhyHsymIdempotentSym a) @e se Refl  type WhyReplace (from :: t) (p :: t ~> Type)                 (y :: t) (e :: from :~: y) = p @@ y@@ -130,7 +134,7 @@         -> p @@ to replace from eq =   withSomeSing eq $ \(singEq :: Sing r) ->-    (~>:~:) @t @from @to @r @(WhyReplaceSym from p) singEq from+    (~>:~:) @t @from @to @(WhyReplaceSym from p) @r singEq from  {- type WhyHreplace (from :: j) (p :: forall (z :: Type). z ~> Type)@@ -175,4 +179,22 @@      -> f @@ a :~: f @@ b cong eq =   withSomeSing eq $ \(singEq :: Sing r) ->-    (~>:~:) @x @a @b @r @(WhyCongSym x y f a) singEq Refl+    (~>:~:) @x @a @b @(WhyCongSym x y f a) @r singEq Refl++type WhyEqIsRefl (a :: k) (z :: k) (e :: a :~: z)+  = e :~~: (Refl :: a :~: a)+data WhyEqIsReflSym (a :: k) :: forall (z :: k). a :~: z ~> Type+type instance Apply (WhyEqIsReflSym a :: a :~: z ~> Type) e = WhyEqIsRefl a z e++eqIsRefl :: forall (k :: Type) (a :: k) (b :: k) (e :: a :~: b).+            Sing e -> e :~~: (Refl :: a :~: a)+eqIsRefl eq = (~>:~:) @k @a @b @(WhyEqIsReflSym a) @e eq HRefl++type WhyHEqIsHRefl (a :: j) (z :: k) (e :: a :~~: z)+  = e :~~: (HRefl :: a :~~: a)+data WhyHEqIsHReflSym (a :: j) :: forall (k :: Type) (z :: k). a :~~: z ~> Type+type instance Apply (WhyHEqIsHReflSym a :: a :~~: z ~> Type) e = WhyHEqIsHRefl a z e++heqIsHRefl :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (e :: a :~~: b).+              Sing e -> e :~~: (HRefl :: a :~~: a)+heqIsHRefl heq = (~>:~~:) @j @k @a @b @(WhyHEqIsHReflSym a) @e heq HRefl

@@ -1,117 +0,0 @@-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeInType #-}-{-# LANGUAGE TypeOperators #-}-module PeanoSpec where--import Data.Kind-import Data.Singletons--import PeanoTypes--import Test.Hspec--main :: IO ()-main = hspec spec--spec :: Spec-spec = parallel $ do-  describe "replicateVec" $ do-    it "works with empty lists" $-      replicateVec SZ () `shouldBe` VNil-    it "works with non-empty lists" $-      replicateVec (SS SZ) () `shouldBe` () :# VNil-  describe "mapVec" $ do-    it "maps over a Vec" $ do-      mapVec reverse ("hello" :# "world" :# VNil)-          `shouldBe` ("olleh" :# "dlrow" :# VNil)-  describe "zipWithVec" $ do-    it "zips two Vecs" $ do-      zipWithVec (,) ((2 :: Int) :# 22 :# VNil)-                     ("chicken-of-the-woods" :# "hen-of-woods" :# VNil)-        `shouldBe` ((2, "chicken-of-the-woods") :# (22, "hen-of-woods")-                                                :# VNil)-  describe "appendVec" $ do-    it "appends two Vecs" $ do-      appendVec ("portabello" :# "bay-bolete"-                              :# "funnel-chantrelle"-                              :# VNil)-                ("sheathed-woodtuft" :# "puffball" :# VNil)-        `shouldBe` ("portabello" :# "bay-bolete"-                                 :# "funnel-chantrelle"-                                 :# "sheathed-woodtuft"-                                 :# "puffball"-                                 :# VNil)-  describe "transposeVec" $ do-    it "transposes a Vec" $ do-      transposeVec (('a' :# 'b' :# 'c' :# VNil)-                 :# ('d' :# 'e' :# 'f' :# VNil)-                 :# VNil)-        `shouldBe`-                   (('a' :# 'd' :# VNil)-                 :# ('b' :# 'e' :# VNil)-                 :# ('c' :# 'f' :# VNil)-                 :# VNil)---------replicateVec :: forall (e :: Type) (howMany :: Peano).-                Sing howMany -> e -> Vec e howMany-replicateVec s e = elimPeano @(TyCon1 (Vec e)) @howMany s VNil step-  where-    step :: forall (k :: Peano). Sing k -> Vec e k -> Vec e (S k)-    step _ = (e :#)--mapVec :: forall (a :: Type) (b :: Type) (n :: Peano).-          SingI n-       => (a -> b) -> Vec a n -> Vec b n-mapVec f = elimPeano @(WhyMapVecSym2 a b) @n (sing @_ @n) base step-  where-    base :: WhyMapVec a b Z-    base _ = VNil--    step :: forall (k :: Peano). Sing k -> WhyMapVec a b k -> WhyMapVec a b (S k)-    step _ mapK vK = f (vhead vK) :# mapK (vtail vK)--zipWithVec :: forall (a :: Type) (b :: Type) (c :: Type) (n :: Peano).-              SingI n-           => (a -> b -> c) -> Vec a n -> Vec b n -> Vec c n-zipWithVec f = elimPeano @(WhyZipWithVecSym3 a b c) @n (sing @_ @n) base step-  where-    base :: WhyZipWithVec a b c Z-    base _ _ = VNil--    step :: forall (k :: Peano).-            Sing k-         -> WhyZipWithVec a b c k-         -> WhyZipWithVec a b c (S k)-    step _ zwK vaK vbK = f   (vhead vaK) (vhead vbK)-                      :# zwK (vtail vaK) (vtail vbK)--appendVec :: forall (e :: Type) (n :: Peano) (m :: Peano).-             SingI n-          => Vec e n -> Vec e m -> Vec e (n `Plus` m)-appendVec = elimPeano @(WhyAppendVecSym2 e m) @n (sing @_ @n) base step-  where-    base :: WhyAppendVec e m Z-    base _ = id--    step :: forall (k :: Peano).-            Sing k-         -> WhyAppendVec e m k-         -> WhyAppendVec e m (S k)-    step _ avK vK1 vK2 = vhead vK1 :# avK (vtail vK1) vK2--transposeVec :: forall (e :: Type) (n :: Peano) (m :: Peano).-                (SingI n, SingI m)-             => Vec (Vec e m) n -> Vec (Vec e n) m-transposeVec = elimPeano @(WhyTransposeVecSym2 e m) @n (sing @_ @n) base step-  where-    base :: WhyTransposeVec e m Z-    base _ = replicateVec (sing @_ @m) VNil--    step :: forall (k :: Peano).-            Sing k-         -> WhyTransposeVec e m k-         -> WhyTransposeVec e m (S k)-    step _ transK vK = zipWithVec (:#) (vhead vK) (transK (vtail vK))

@@ -1,94 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeInType #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}-module PeanoTypes where--import Data.Eliminator.TH-import Data.Kind-import Data.Singletons.TH--$(singletons [d|-  data Peano = Z | S Peano--  infixl 6 `plus`-  plus :: Peano -> Peano -> Peano-  plus Z     m = m-  plus (S k) m = S (plus k m)--  infixl 7 `times`-  times :: Peano -> Peano -> Peano-  times Z     _ = Z-  times (S k) m = plus m (times k m)-  |])-$(deriveElim ''Peano)--data Vec a (n :: Peano) where-  VNil :: Vec a Z-  (:#) :: { vhead :: a, vtail :: Vec a n } -> Vec a (S n)-infixr 5 :#-deriving instance Eq a   => Eq (Vec a n)-deriving instance Ord a  => Ord (Vec a n)-deriving instance Show a => Show (Vec a n)--data instance Sing (z :: Vec a n) where-  SVNil :: Sing VNil-  (:%#) :: { sVhead :: Sing x, sVtail :: Sing xs } -> Sing (x :# xs)-type SVec = (Sing :: Vec a n -> Type)-infixr 5 :%#--instance SingKind a => SingKind (Vec a n) where-  type Demote (Vec a n) = Vec (Demote a) n-  fromSing SVNil      = VNil-  fromSing (x :%# xs) = fromSing x :# fromSing xs-  toSing VNil = SomeSing SVNil-  toSing (x :# xs) =-    withSomeSing x $ \sx ->-      withSomeSing xs $ \sxs ->-        SomeSing $ sx :%# sxs--instance SingI VNil where-  sing = SVNil--instance (SingI x, SingI xs) => SingI (x :# xs) where-  sing = sing :%# sing--elimVec :: forall (a :: Type) (n :: Peano)-                  (p :: forall (k :: Peano). Vec a k ~> Type) (v :: Vec a n).-           Sing v-        -> p @@ VNil-        -> (forall (k :: Peano) (x :: a) (xs :: Vec a k).-                   Sing x -> Sing xs -> p @@ xs -> p @@ (x :# xs))-        -> p @@ v-elimVec SVNil pVNil _ = pVNil-elimVec (sx :%# (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =-  pVCons sx sxs (elimVec @a @k @p @xs sxs pVNil pVCons)--type WhyMapVec (a :: Type) (b :: Type) (n :: Peano) = Vec a n -> Vec b n-$(genDefunSymbols [''WhyMapVec])--type WhyZipWithVec (a :: Type) (b :: Type) (c :: Type) (n :: Peano)-  = Vec a n -> Vec b n -> Vec c n-$(genDefunSymbols [''WhyZipWithVec])--type WhyAppendVec (e :: Type) (m :: Peano) (n :: Peano)-  = Vec e n -> Vec e m -> Vec e (n `Plus` m)-$(genDefunSymbols [''WhyAppendVec])--type WhyTransposeVec (e :: Type) (m :: Peano) (n :: Peano)-  = Vec (Vec e m) n -> Vec (Vec e n) m-$(genDefunSymbols [''WhyTransposeVec])--type WhyConcatVec (e :: Type) (j :: Peano) (n :: Peano) (l :: Vec (Vec e j) n)-  = Vec e (n `Times` j)-data WhyConcatVecSym (e :: Type) (j :: Peano)-  :: forall (n :: Peano). Vec (Vec e j) n ~> Type-type instance Apply (WhyConcatVecSym e j :: Vec (Vec e j) n ~> Type) l-  = WhyConcatVec e j n l

@@ -5,11 +5,13 @@ {-# LANGUAGE TypeOperators #-} module VecSpec where +import Data.Eliminator import Data.Kind+import Data.Nat import Data.Singletons+import Data.Singletons.Prelude.Num -import PeanoSpec (appendVec)-import PeanoTypes+import VecTypes  import Test.Hspec @@ -18,6 +20,43 @@  spec :: Spec spec = parallel $ do+  describe "replicateVec" $ do+    it "works with empty lists" $+      replicateVec (sLit @0) () `shouldBe` VNil+    it "works with non-empty lists" $ do+      replicateVec (sLit @1) () `shouldBe` () :# VNil+      replicateVec (sLit @2) () `shouldBe` () :# () :# VNil+  describe "mapVec" $ do+    it "maps over a Vec" $ do+      mapVec reverse ("hello" :# "world" :# VNil)+          `shouldBe` ("olleh" :# "dlrow" :# VNil)+  describe "zipWithVec" $ do+    it "zips two Vecs" $ do+      zipWithVec (,) ((2 :: Int) :# 22 :# VNil)+                     ("chicken-of-the-woods" :# "hen-of-woods" :# VNil)+        `shouldBe` ((2, "chicken-of-the-woods") :# (22, "hen-of-woods")+                                                :# VNil)+  describe "appendVec" $ do+    it "appends two Vecs" $ do+      appendVec ("portabello" :# "bay-bolete"+                              :# "funnel-chantrelle"+                              :# VNil)+                ("sheathed-woodtuft" :# "puffball" :# VNil)+        `shouldBe` ("portabello" :# "bay-bolete"+                                 :# "funnel-chantrelle"+                                 :# "sheathed-woodtuft"+                                 :# "puffball"+                                 :# VNil)+  describe "transposeVec" $ do+    it "transposes a Vec" $ do+      transposeVec (('a' :# 'b' :# 'c' :# VNil)+                 :# ('d' :# 'e' :# 'f' :# VNil)+                 :# VNil)+        `shouldBe`+                   (('a' :# 'd' :# VNil)+                 :# ('b' :# 'e' :# VNil)+                 :# ('c' :# 'f' :# VNil)+                 :# VNil)   describe "concatVec" $ do     it "concats a Vec of Vecs" $ do       concatVec ((False :# True  :# False :# VNil)@@ -28,16 +67,77 @@  ----- -concatVec :: forall (e :: Type) (n :: Peano) (j :: Peano).+replicateVec :: forall (e :: Type) (howMany :: Nat).+                Sing howMany -> e -> Vec e howMany+replicateVec s e = elimNat @(TyCon1 (Vec e)) @howMany s VNil step+  where+    step :: forall (k :: Nat). Sing k -> Vec e k -> Vec e (S k)+    step _ = (e :#)++mapVec :: forall (a :: Type) (b :: Type) (n :: Nat).+          SingI n+       => (a -> b) -> Vec a n -> Vec b n+mapVec f = elimNat @(WhyMapVecSym2 a b) @n (sing @_ @n) base step+  where+    base :: WhyMapVec a b Z+    base _ = VNil++    step :: forall (k :: Nat). Sing k -> WhyMapVec a b k -> WhyMapVec a b (S k)+    step _ mapK vK = f (vhead vK) :# mapK (vtail vK)++zipWithVec :: forall (a :: Type) (b :: Type) (c :: Type) (n :: Nat).+              SingI n+           => (a -> b -> c) -> Vec a n -> Vec b n -> Vec c n+zipWithVec f = elimNat @(WhyZipWithVecSym3 a b c) @n (sing @_ @n) base step+  where+    base :: WhyZipWithVec a b c Z+    base _ _ = VNil++    step :: forall (k :: Nat).+            Sing k+         -> WhyZipWithVec a b c k+         -> WhyZipWithVec a b c (S k)+    step _ zwK vaK vbK = f   (vhead vaK) (vhead vbK)+                      :# zwK (vtail vaK) (vtail vbK)++appendVec :: forall (e :: Type) (n :: Nat) (m :: Nat).+             SingI n+          => Vec e n -> Vec e m -> Vec e (n :+ m)+appendVec = elimNat @(WhyAppendVecSym2 e m) @n (sing @_ @n) base step+  where+    base :: WhyAppendVec e m Z+    base _ = id++    step :: forall (k :: Nat).+            Sing k+         -> WhyAppendVec e m k+         -> WhyAppendVec e m (S k)+    step _ avK vK1 vK2 = vhead vK1 :# avK (vtail vK1) vK2++transposeVec :: forall (e :: Type) (n :: Nat) (m :: Nat).+                (SingI n, SingI m)+             => Vec (Vec e m) n -> Vec (Vec e n) m+transposeVec = elimNat @(WhyTransposeVecSym2 e m) @n (sing @_ @n) base step+  where+    base :: WhyTransposeVec e m Z+    base _ = replicateVec (sing @_ @m) VNil++    step :: forall (k :: Nat).+            Sing k+         -> WhyTransposeVec e m k+         -> WhyTransposeVec e m (S k)+    step _ transK vK = zipWithVec (:#) (vhead vK) (transK (vtail vK))++concatVec :: forall (e :: Type) (n :: Nat) (j :: Nat).              (SingKind e, SingI j, e ~ Demote e)-          => Vec (Vec e j) n -> Vec e (n `Times` j)+          => Vec (Vec e j) n -> Vec e (n :* j) concatVec l = withSomeSing l $ \(singL :: Sing l) ->                 elimVec @(Vec e j) @n @(WhyConcatVecSym e j) @l singL base step   where     base :: WhyConcatVec e j Z VNil     base = VNil -    step :: forall (k :: Peano) (x :: Vec e j) (xs :: Vec (Vec e j) k).+    step :: forall (k :: Nat) (x :: Vec e j) (xs :: Vec (Vec e j) k).                    Sing x -> Sing xs                 -> WhyConcatVec e j k     xs                 -> WhyConcatVec e j (S k) (x :# xs)

@@ -0,0 +1,80 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+module VecTypes where++import Data.Kind+import Data.Nat+import Data.Singletons.Prelude.Num+import Data.Singletons.TH++data Vec :: Type -> Nat -> Type where+  VNil :: Vec a Z+  (:#) :: { vhead :: a, vtail :: Vec a n } -> Vec a (S n)+infixr 5 :#+deriving instance Eq a   => Eq (Vec a n)+deriving instance Ord a  => Ord (Vec a n)+deriving instance Show a => Show (Vec a n)++data instance Sing (z :: Vec a n) where+  SVNil :: Sing VNil+  (:%#) :: { sVhead :: Sing x, sVtail :: Sing xs } -> Sing (x :# xs)+type SVec = (Sing :: Vec a n -> Type)+infixr 5 :%#++instance SingKind a => SingKind (Vec a n) where+  type Demote (Vec a n) = Vec (Demote a) n+  fromSing SVNil      = VNil+  fromSing (x :%# xs) = fromSing x :# fromSing xs+  toSing VNil = SomeSing SVNil+  toSing (x :# xs) =+    withSomeSing x $ \sx ->+      withSomeSing xs $ \sxs ->+        SomeSing $ sx :%# sxs++instance SingI VNil where+  sing = SVNil++instance (SingI x, SingI xs) => SingI (x :# xs) where+  sing = sing :%# sing++elimVec :: forall (a :: Type) (n :: Nat)+                  (p :: forall (k :: Nat). Vec a k ~> Type) (v :: Vec a n).+           Sing v+        -> p @@ VNil+        -> (forall (k :: Nat) (x :: a) (xs :: Vec a k).+                   Sing x -> Sing xs -> p @@ xs -> p @@ (x :# xs))+        -> p @@ v+elimVec SVNil pVNil _ = pVNil+elimVec (sx :%# (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =+  pVCons sx sxs (elimVec @a @k @p @xs sxs pVNil pVCons)++type WhyMapVec (a :: Type) (b :: Type) (n :: Nat) = Vec a n -> Vec b n+$(genDefunSymbols [''WhyMapVec])++type WhyZipWithVec (a :: Type) (b :: Type) (c :: Type) (n :: Nat)+  = Vec a n -> Vec b n -> Vec c n+$(genDefunSymbols [''WhyZipWithVec])++type WhyAppendVec (e :: Type) (m :: Nat) (n :: Nat)+  = Vec e n -> Vec e m -> Vec e (n :+ m)+$(genDefunSymbols [''WhyAppendVec])++type WhyTransposeVec (e :: Type) (m :: Nat) (n :: Nat)+  = Vec (Vec e m) n -> Vec (Vec e n) m+$(genDefunSymbols [''WhyTransposeVec])++type WhyConcatVec (e :: Type) (j :: Nat) (n :: Nat) (l :: Vec (Vec e j) n)+  = Vec e (n :* j)+data WhyConcatVecSym (e :: Type) (j :: Nat)+  :: forall (n :: Nat). Vec (Vec e j) n ~> Type+type instance Apply (WhyConcatVecSym e j :: Vec (Vec e j) n ~> Type) l+  = WhyConcatVec e j n l