packages feed

eliminators (empty) → 0.1

raw patch · 14 files changed

+1247/−0 lines, 14 filesdep +basedep +eliminatorsdep +hspecsetup-changed

Dependencies added: base, eliminators, hspec, singletons

Files

+ CHANGELOG.md view
@@ -0,0 +1,2 @@+# 0.1 [2017-07-02]+* Initial release.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2017, Ryan Scott++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Ryan Scott nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,18 @@+# `eliminators`+[![Hackage](https://img.shields.io/hackage/v/eliminators.svg)][Hackage: eliminators]+[![Hackage Dependencies](https://img.shields.io/hackage-deps/v/eliminators.svg)](http://packdeps.haskellers.com/reverse/eliminators)+[![Haskell Programming Language](https://img.shields.io/badge/language-Haskell-blue.svg)][Haskell.org]+[![BSD3 License](http://img.shields.io/badge/license-BSD3-brightgreen.svg)][tl;dr Legal: BSD3]+[![Build](https://img.shields.io/travis/RyanGlScott/eliminators.svg)](https://travis-ci.org/RyanGlScott/eliminators)++[Hackage: eliminators]:+  http://hackage.haskell.org/package/eliminators+  "eliminators package on Hackage"+[Haskell.org]:+  http://www.haskell.org+  "The Haskell Programming Language"+[tl;dr Legal: BSD3]:+  https://tldrlegal.com/license/bsd-3-clause-license-%28revised%29+  "BSD 3-Clause License (Revised)"++This library provides eliminators for inductive data types, leveraging the power of the `singletons` library to allow dependently typed elimination.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ eliminators.cabal view
@@ -0,0 +1,49 @@+name:                eliminators+version:             0.1+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+                     dependently typed elimination.+homepage:            https://github.com/RyanGlScott/eliminators+bug-reports:         https://github.com/RyanGlScott/eliminators/issues+license:             BSD3+license-file:        LICENSE+author:              Ryan Scott+maintainer:          Ryan Scott <ryan.gl.scott@gmail.com>+stability:           Experimental+copyright:           (C) 2017 Ryan Scott+category:            Dependent Types+build-type:          Simple+extra-source-files:  CHANGELOG.md, README.md+cabal-version:       >=1.10+tested-with:         GHC == 8.2.1++source-repository head+  type:                git+  location:            https://github.com/RyanGlScott/eliminators++library+  exposed-modules:     Data.Eliminator+  build-depends:       base       >= 4.10 && < 4.11+                     , singletons >= 2.3  && < 2.4+  hs-source-dirs:      src+  default-language:    Haskell2010+  ghc-options:         -Wall -Wno-unticked-promoted-constructors++test-suite spec+  type:                exitcode-stdio-1.0+  main-is:             Spec.hs+  other-modules:       EqualitySpec+                       GADTSpec+                       ListSpec+                       ListTypes+                       PeanoSpec+                       PeanoTypes+                       VecSpec+  build-depends:       base       >= 4.10 && < 4.11+                     , eliminators+                     , hspec      >= 2    && < 3+                     , singletons >= 2.3  && < 2.4+  hs-source-dirs:      tests+  default-language:    Haskell2010+  ghc-options:         -Wall -Wno-unticked-promoted-constructors -threaded -rtsopts
+ src/Data/Eliminator.hs view
@@ -0,0 +1,510 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-|+Module:      Data.Eliminator+Copyright:   (C) 2017 Ryan Scott+License:     BSD-style (see the file LICENSE)+Maintainer:  Ryan Scott+Stability:   Experimental+Portability: GHC++Dependently typed elimination functions using @singletons@.+-}+module Data.Eliminator (+    -- * Eliminator functions+    -- ** Eliminators using '(->)'+    -- $eliminators+    elimBool+  , elimEither+  , elimList+  , elimMaybe+  , elimNat+  , elimNonEmpty+  , elimOrdering+  , elimTuple0+  , elimTuple2+  , elimTuple3+  , elimTuple4+  , elimTuple5+  , elimTuple6+  , elimTuple7++    -- ** Eliminators using '(~>)'+    -- $eliminators-TyFun+  , elimBoolTyFun+  , elimEitherTyFun+  , elimListTyFun+  , elimMaybeTyFun+  , elimNatTyFun+  , elimNonEmptyTyFun+  , elimOrderingTyFun+  , elimTuple0TyFun+  , elimTuple2TyFun+  , elimTuple3TyFun+  , elimTuple4TyFun+  , elimTuple5TyFun+  , elimTuple6TyFun+  , elimTuple7TyFun++    -- ** Arrow-polymorphic eliminators (very experimental)+    -- $eliminators-Poly+  , FunArrow(..)+  , FunType(..)+  , type (-?>)+  , AppType(..)+  , FunApp++  , elimBoolPoly+  , elimEitherPoly+  , elimListPoly+  , elimMaybePoly+  , elimNonEmptyPoly+  , elimNatPoly+  , elimOrderingPoly+  , elimTuple0Poly+  , elimTuple2Poly+  , elimTuple3Poly+  , elimTuple4Poly+  , elimTuple5Poly+  , elimTuple6Poly+  , elimTuple7Poly+  ) where++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 Unsafe.Coerce (unsafeCoerce)++{- $eliminators++These eliminators are defined with propositions of kind @\<Datatype\> -> 'Type'@+(that is, using the '(->)' kind). As a result, these eliminators' type signatures+are the most readable in this library, and most closely resemble eliminator functions+in other dependently typed languages.+-}++elimBool :: forall (p :: Bool -> Type) (b :: Bool).+            Sing b+         -> p False+         -> p True+         -> p b+elimBool = elimBoolPoly @(:->)++elimEither :: forall (a :: Type) (b :: Type) (p :: Either a b -> Type) (e :: Either a b).+              Sing e+           -> (forall (l :: a). Sing l -> p (Left  l))+           -> (forall (r :: b). Sing r -> p (Right r))+           -> p e+elimEither = elimEitherPoly @(:->)++elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).+            Sing l+         -> p '[]+         -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))+         -> p l+elimList = elimListPoly @(:->)++elimMaybe :: forall (a :: Type) (p :: Maybe a -> Type) (m :: Maybe a).+             Sing m+          -> p Nothing+          -> (forall (x :: a). Sing x -> p (Just x))+          -> p m+elimMaybe = elimMaybePoly @(:->)++elimNat :: forall (p :: Nat -> Type) (n :: Nat).+           Sing n+        -> p 0+        -> (forall (k :: Nat). Sing k -> p k -> p (k :+ 1))+        -> p n+elimNat = elimNatPoly @(:->)++elimNonEmpty :: forall (a :: Type) (p :: NonEmpty a -> Type) (n :: NonEmpty a).+                Sing n+             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p (x :| xs))+             -> p n+elimNonEmpty = elimNonEmptyPoly @(:->)++elimOrdering :: forall (p :: Ordering -> Type) (o :: Ordering).+                Sing o+             -> p LT+             -> p EQ+             -> p GT+             -> p o+elimOrdering = elimOrderingPoly @(:->)++elimTuple0 :: forall (p :: () -> Type) (u :: ()).+              Sing u+           -> p '()+           -> p u+elimTuple0 = elimTuple0Poly @(:->)++elimTuple2 :: forall (a :: Type) (b :: Type)+                     (p :: (a, b) -> Type) (t :: (a, b)).+              Sing t+           -> (forall (aa :: a) (bb :: b).+                      Sing aa -> Sing bb+                   -> p '(aa, bb))+           -> p t+elimTuple2 = elimTuple2Poly @(:->)++elimTuple3 :: forall (a :: Type) (b :: Type) (c :: Type)+                     (p :: (a, b, c) -> Type) (t :: (a, b, c)).+              Sing t+           -> (forall (aa :: a) (bb :: b) (cc :: c).+                      Sing aa -> Sing bb -> Sing cc+                   -> p '(aa, bb, cc))+           -> p t+elimTuple3 = elimTuple3Poly @(:->)++elimTuple4 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type)+                     (p :: (a, b, c, d) -> Type) (t :: (a, b, c, d)).+              Sing t+           -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d).+                      Sing aa -> Sing bb -> Sing cc -> Sing dd+                   -> p '(aa, bb, cc, dd))+           -> p t+elimTuple4 = elimTuple4Poly @(:->)++elimTuple5 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type)+                     (p :: (a, b, c, d, e) -> Type) (t :: (a, b, c, d, e)).+              Sing t+           -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e).+                      Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee+                   -> p '(aa, bb, cc, dd, ee))+           -> p t+elimTuple5 = elimTuple5Poly @(:->)++elimTuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type)+                     (p :: (a, b, c, d, e, f) -> Type) (t :: (a, b, c, d, e, f)).+              Sing t+           -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f).+                      Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff+                   -> p '(aa, bb, cc, dd, ee, ff))+           -> p t+elimTuple6 = elimTuple6Poly @(:->)++elimTuple7 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type)+                     (p :: (a, b, c, d, e, f, g) -> Type) (t :: (a, b, c, d, e, f, g)).+              Sing t+           -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f) (gg :: g).+                      Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> Sing gg+                   -> p '(aa, bb, cc, dd, ee, ff, gg))+           -> p t+elimTuple7 = elimTuple7Poly @(:->)++{- $eliminators-TyFun++These eliminators are defined with propositions of kind @\<Datatype\> ~> 'Type'@+(that is, using the '(~>)' kind). These eliminators are designed for+defunctionalized (i.e., \"partially applied\") type families as predicates,+and as a result, the predicates must be applied manually with '(@@)'.+-}++elimBoolTyFun :: forall (p :: Bool ~> Type) (b :: Bool).+                 Sing b+              -> p @@ False+              -> p @@ True+              -> p @@ b+elimBoolTyFun = elimBoolPoly @(:~>) @p++elimEitherTyFun :: forall (a :: Type) (b :: Type) (p :: Either a b ~> Type) (e :: Either a b).+                   Sing e+                -> (forall (l :: a). Sing l -> p @@ (Left  l))+                -> (forall (r :: b). Sing r -> p @@ (Right r))+                -> p @@ e+elimEitherTyFun = elimEitherPoly @(:~>) @_ @_ @p++elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).+                 Sing l+              -> p @@ '[]+              -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))+              -> p @@ l+elimListTyFun = elimListPoly @(:~>) @_ @p++elimMaybeTyFun :: forall (a :: Type) (p :: Maybe a ~> Type) (m :: Maybe a).+                  Sing m+               -> p @@ Nothing+               -> (forall (x :: a). Sing x -> p @@ (Just x))+               -> p @@ m+elimMaybeTyFun = elimMaybePoly @(:~>) @_ @p++elimNatTyFun :: forall (p :: Nat ~> Type) (n :: Nat).+                Sing n+             -> p @@ 0+             -> (forall (k :: Nat). Sing k -> p @@ k -> p @@ (k :+ 1))+             -> p @@ n+elimNatTyFun = elimNatPoly @(:~>) @p++elimNonEmptyTyFun :: forall (a :: Type) (p :: NonEmpty a ~> Type) (n :: NonEmpty a).+                     Sing n+                  -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ (x :| xs))+                  -> p @@ n+elimNonEmptyTyFun = elimNonEmptyPoly @(:~>) @_ @p++elimOrderingTyFun :: forall (p :: Ordering ~> Type) (o :: Ordering).+                     Sing o+                  -> p @@ LT+                  -> p @@ EQ+                  -> p @@ GT+                  -> p @@ o+elimOrderingTyFun = elimOrderingPoly @(:~>) @p++elimTuple0TyFun :: forall (p :: () ~> Type) (u :: ()).+                   Sing u+                -> p @@ '()+                -> p @@ u+elimTuple0TyFun = elimTuple0Poly @(:~>) @p++elimTuple2TyFun :: forall (a :: Type) (b :: Type)+                          (p :: (a, b) ~> Type) (t :: (a, b)).+                   Sing t+                -> (forall (aa :: a) (bb :: b).+                           Sing aa -> Sing bb+                        -> p @@ '(aa, bb))+                -> p @@ t+elimTuple2TyFun = elimTuple2Poly @(:~>) @_ @_ @p++elimTuple3TyFun :: forall (a :: Type) (b :: Type) (c :: Type)+                          (p :: (a, b, c) ~> Type) (t :: (a, b, c)).+                   Sing t+                -> (forall (aa :: a) (bb :: b) (cc :: c).+                           Sing aa -> Sing bb -> Sing cc+                        -> p @@ '(aa, bb, cc))+                -> p @@ t+elimTuple3TyFun = elimTuple3Poly @(:~>) @_ @_ @_ @p++elimTuple4TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type)+                          (p :: (a, b, c, d) ~> Type) (t :: (a, b, c, d)).+                   Sing t+                -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d).+                           Sing aa -> Sing bb -> Sing cc -> Sing dd+                        -> p @@ '(aa, bb, cc, dd))+                -> p @@ t+elimTuple4TyFun = elimTuple4Poly @(:~>) @_ @_ @_ @_ @p++elimTuple5TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type)+                          (p :: (a, b, c, d, e) ~> Type) (t :: (a, b, c, d, e)).+                   Sing t+                -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e).+                           Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee+                        -> p @@ '(aa, bb, cc, dd, ee))+                -> p @@ t+elimTuple5TyFun = elimTuple5Poly @(:~>) @_ @_ @_ @_ @_ @p++elimTuple6TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type)+                          (p :: (a, b, c, d, e, f) ~> Type) (t :: (a, b, c, d, e, f)).+                   Sing t+                -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f).+                           Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff+                        -> p @@ '(aa, bb, cc, dd, ee, ff))+                -> p @@ t+elimTuple6TyFun = elimTuple6Poly @(:~>) @_ @_ @_ @_ @_ @_ @p++elimTuple7TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type)+                          (p :: (a, b, c, d, e, f, g) ~> Type) (t :: (a, b, c, d, e, f, g)).+                   Sing t+                -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f) (gg :: g).+                           Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> Sing gg+                        -> p @@ '(aa, bb, cc, dd, ee, ff, gg))+                -> p @@ t+elimTuple7TyFun = elimTuple7Poly @(:~>) @_ @_ @_ @_ @_ @_ @_ @p++{- $eliminators-Poly++Eliminators using '(->)' and eliminators using '(~>)' end up having very similar+implementations - so similar, in fact, that they can be generalized to be polymorphic+over the arrow kind used (as well as the application operator). The 'FunType' and+'AppType' classes capture these notions of abstraction and application, respectively.++Not all eliminators are known to work under this generalized scheme yet (for+instance, eliminators for GADTs).++Chances are, you won't want to use these eliminators directly, since their type+signatures are pretty horrific and don't always play well with type inference.+However, they are provided for the sake of completeness.+-}++-- | An enumeration which represents the possible choices of arrow kind for+-- eliminator functions.+data FunArrow = (:->) -- ^ '(->)'+              | (:~>) -- ^ '(~>)'++-- | Things which have arrow kinds.+class FunType (arr :: FunArrow) where+  -- | An arrow kind.+  type Fun (k1 :: Type) arr (k2 :: Type) :: Type++-- | Things which can be applied.+class FunType arr => AppType (arr :: FunArrow) where+  -- | An application of a 'Fun' to an argument.+  --+  -- Note that this can't be defined in the same class as 'Fun' due to GHC+  -- restrictions on associated type families.+  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2++-- | Something which has both a 'Fun' and an 'App'.+type FunApp arr = (FunType arr, AppType arr)++instance FunType (:->) where+  type Fun k1 (:->) k2 = k1 -> k2++instance AppType (:->) where+  type App k1 (:->) k2 (f :: k1 -> k2) x = f x++instance FunType (:~>) where+  type Fun k1 (:~>) k2 = k1 ~> k2++instance AppType (:~>) where+  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x++-- | An infix synonym for 'Fun'.+infixr 0 -?>+type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2++-- Note: it would be nice to have an infix synonym for 'App' as well, but+-- the order in which the type variable dependencies occur makes this awkward+-- to achieve.++elimBoolPoly :: forall (arr :: FunArrow) (p :: (Bool -?> Type) arr) (b :: Bool).+                FunApp arr+             => Sing b+             -> App Bool arr Type p False+             -> App Bool arr Type p True+             -> App Bool arr Type p b+elimBoolPoly SFalse pF _  = pF+elimBoolPoly STrue  _  pT = pT++elimEitherPoly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (p :: (Either a b -?> Type) arr) (e :: Either a b).+                  FunApp arr+               => Sing e+               -> (forall (l :: a). Sing l -> App (Either a b) arr Type p (Left  l))+               -> (forall (r :: b). Sing r -> App (Either a b) arr Type p (Right r))+               -> App (Either a b) arr Type p e+elimEitherPoly (SLeft  sl) pLeft _  = pLeft  sl+elimEitherPoly (SRight sr) _ pRight = pRight sr++elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).+                FunApp arr+             => Sing l+             -> App [a] arr Type p '[]+             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))+             -> App [a] arr Type p l+elimListPoly SNil                      pNil _     = pNil+elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)++elimMaybePoly :: forall (arr :: FunArrow) (a :: Type) (p :: (Maybe a -?> Type) arr) (m :: Maybe a).+                 FunApp arr+              => Sing m+              -> App (Maybe a) arr Type p Nothing+              -> (forall (x :: a). Sing x -> App (Maybe a) arr Type p (Just x))+              -> App (Maybe a) arr Type p m+elimMaybePoly SNothing pNothing _ = pNothing+elimMaybePoly (SJust sx) _ pJust  = pJust sx++elimNatPoly :: forall (arr :: FunArrow) (p :: (Nat -?> Type) arr) (n :: Nat).+               FunApp arr+            => Sing n+            -> App Nat arr Type p 0+            -> (forall (k :: Nat). Sing k -> App Nat arr Type p k -> App Nat arr Type p (k :+ 1))+            -> App Nat arr Type p n+elimNatPoly snat pZ pS =+  case fromSing snat of+    0        -> unsafeCoerce pZ+    nPlusOne -> case toSing (pred nPlusOne) of+                  SomeSing (sn :: Sing k) -> unsafeCoerce (pS sn (elimNatPoly @arr @p @k sn pZ pS))++elimNonEmptyPoly :: forall (arr :: FunArrow) (a :: Type) (p :: (NonEmpty a -?> Type) arr) (n :: NonEmpty a).+                    FunApp arr+                 => Sing n+                 -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App (NonEmpty a) arr Type p (x :| xs))+                 -> App (NonEmpty a) arr Type p n+elimNonEmptyPoly (sx :%| sxs) pNECons = pNECons sx sxs++elimOrderingPoly :: forall (arr :: FunArrow) (p :: (Ordering -?> Type) arr) (o :: Ordering).+                    Sing o+                 -> App Ordering arr Type p LT+                 -> App Ordering arr Type p EQ+                 -> App Ordering arr Type p GT+                 -> App Ordering arr Type p o+elimOrderingPoly SLT pLT _   _   = pLT+elimOrderingPoly SEQ _   pEQ _   = pEQ+elimOrderingPoly SGT _   _   pGT = pGT++elimTuple0Poly :: forall (arr :: FunArrow) (p :: (() -?> Type) arr) (u :: ()).+                  FunApp arr+               => Sing u+               -> App () arr Type p '()+               -> App () arr Type p u+elimTuple0Poly STuple0 pTuple0 = pTuple0++elimTuple2Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type)+                         (p :: ((a, b) -?> Type) arr) (t :: (a, b)).+                  FunApp arr+               => Sing t+               -> (forall (aa :: a) (bb :: b).+                          Sing aa -> Sing bb+                       -> App (a, b) arr Type p '(aa, bb))+               -> App (a, b) arr Type p t+elimTuple2Poly (STuple2 sa sb) pTuple2 = pTuple2 sa sb++elimTuple3Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type)+                         (p :: ((a, b, c) -?> Type) arr) (t :: (a, b, c)).+                  FunApp arr+               => Sing t+               -> (forall (aa :: a) (bb :: b) (cc :: c).+                          Sing aa -> Sing bb -> Sing cc+                       -> App (a, b, c) arr Type p '(aa, bb, cc))+               -> App (a, b, c) arr Type p t+elimTuple3Poly (STuple3 sa sb sc) pTuple3 = pTuple3 sa sb sc++elimTuple4Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type)+                         (p :: ((a, b, c, d) -?> Type) arr) (t :: (a, b, c, d)).+                  FunApp arr+               => Sing t+               -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d).+                          Sing aa -> Sing bb -> Sing cc -> Sing dd+                       -> App (a, b, c, d) arr Type p '(aa, bb, cc, dd))+               -> App (a, b, c, d) arr Type p t+elimTuple4Poly (STuple4 sa sb sc sd) pTuple4 = pTuple4 sa sb sc sd++elimTuple5Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type)+                         (p :: ((a, b, c, d, e) -?> Type) arr) (t :: (a, b, c, d, e)).+                  FunApp arr+               => Sing t+               -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e).+                          Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee+                       -> App (a, b, c, d, e) arr Type p '(aa, bb, cc, dd, ee))+               -> App (a, b, c, d, e) arr Type p t+elimTuple5Poly (STuple5 sa sb sc sd se) pTuple5 = pTuple5 sa sb sc sd se++elimTuple6Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type)+                         (p :: ((a, b, c, d, e, f) -?> Type) arr) (t :: (a, b, c, d, e, f)).+                  FunApp arr+               => Sing t+               -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f).+                          Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff+                       -> App (a, b, c, d, e, f) arr Type p '(aa, bb, cc, dd, ee, ff))+               -> App (a, b, c, d, e, f) arr Type p t+elimTuple6Poly (STuple6 sa sb sc sd se sf) pTuple6 = pTuple6 sa sb sc sd se sf++elimTuple7Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type)+                         (p :: ((a, b, c, d, e, f, g) -?> Type) arr) (t :: (a, b, c, d, e, f, g)).+                  FunApp arr+               => Sing t+               -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f) (gg :: g).+                          Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> Sing gg+                       -> App (a, b, c, d, e, f, g) arr Type p '(aa, bb, cc, dd, ee, ff, gg))+               -> App (a, b, c, d, e, f, g) arr Type p t+elimTuple7Poly (STuple7 sa sb sc sd se sf sg) pTuple7 = pTuple7 sa sb sc sd se sf sg
+ tests/EqualitySpec.hs view
@@ -0,0 +1,198 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module EqualitySpec where++import           Data.Eliminator+import           Data.Kind+import           Data.Singletons+import qualified Data.Type.Equality as DTE+import           Data.Type.Equality ((:~:)(..), (:~~:)(..))++import           Test.Hspec++main :: IO ()+main = hspec spec++spec :: Spec+spec = parallel $ do+  describe "sym" $+    it "behaves like the one from Data.Type.Equality" $ do+      let boolEq :: Bool :~: Bool+          boolEq = Refl+      sym boolEq       `shouldBe` DTE.sym boolEq+      sym (sym boolEq) `shouldBe` DTE.sym (DTE.sym boolEq)++-----++data instance Sing (z :: a :~: b) where+  SRefl :: Sing Refl++instance SingKind (a :~: b) where+  type Demote (a :~: b) = a :~: b+  fromSing SRefl = Refl+  toSing Refl    = SomeSing SRefl++instance SingI Refl where+  sing = SRefl++(->:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y -> Type).+           Sing r+        -> p Refl+        -> p r+(->:~:) SRefl pRefl = pRefl++(~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).+           Sing r+        -> p @@ Refl+        -> p @@ r+(~>:~:) SRefl pRefl = pRefl++-- (-?>:~:)++data instance Sing (z :: a :~~: b) where+  SHRefl :: Sing HRefl++instance SingKind (a :~~: b) where+  type Demote (a :~~: b) = a :~~: b+  fromSing SHRefl = HRefl+  toSing HRefl    = SomeSing SHRefl++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).+            Sing r+         -> p HRefl+         -> p r+(->:~~:) SHRefl pHRefl = pHRefl++{-+This doesn't typecheck at the moment due to GHC Trac #13879.+TODO: Uncomment this when the fix becomes available.++(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y ~> Type).+            Sing r+         -> p @@ HRefl+         -> p @@ r+(~>:~~:) SHRefl pHRefl = pHRefl+-}++-- (-?>:~~:)++-----++type WhySym (a :: t) (y :: t) (e :: a :~: y) = y :~: a+data WhySymSym (a :: t) :: forall (y :: t). a :~: y ~> Type+type instance Apply (WhySymSym z :: z :~: y ~> Type) x+  = WhySym z y x++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++type family Symmetry (x :: (a :: k) :~: (b :: k)) :: b :~: a where+  Symmetry Refl = Refl++type WhySymIdempotent (a :: t) (z :: t) (r :: a :~: z)+  = Symmetry (Symmetry r) :~: r+data WhySymIdempotentSym (a :: t) :: forall (z :: t). a :~: z ~> Type+type instance Apply (WhySymIdempotentSym a :: a :~: z ~> Type) r+  = WhySymIdempotent a z r++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++type WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)+                    (y :: t) (e :: from :~: y) = App t arr Type p y+data WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)+  :: forall (y :: t). from :~: y ~> Type+type instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x+  = WhyReplacePoly arr from p y x++replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type).+           p from+        -> from :~: to+        -> p to+replace = replacePoly @(:->)++replaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).+                p @@ from+             -> from :~: to+             -> p @@ to+replaceTyFun = replacePoly @(:~>) @_ @_ @_ @p++replacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t)+                      (p :: (t -?> Type) arr).+               FunApp arr+            => App t arr Type p from+            -> from :~: to+            -> App t arr Type p to+replacePoly from eq =+  withSomeSing eq $ \(singEq :: Sing r) ->+    (~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from++type WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t)+  = App t arr Type f a -> App t arr Type f z+data WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t)+  :: t ~> Type+type instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z++leibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t).+           a :~: b+        -> f a+        -> f b+leibniz = leibnizPoly @(:->)++leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).+                a :~: b+             -> f @@ a+             -> f @@ b+leibnizTyFun = leibnizPoly @(:~>) @_ @f++leibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr)+                      (a :: t) (b :: t).+               FunApp arr+            => a :~: b+            -> App t arr Type f a+            -> App t arr Type f b+leibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id++type WhyCongPoly (arr :: FunArrow) (x :: Type) (y :: Type) (f :: (x -?> y) arr)+                 (a :: x) (z :: x) (e :: a :~: z)+  = App x arr y f a :~: App x arr y f z+data WhyCongPolySym (arr :: FunArrow) (x :: Type) (y :: Type) (f :: (x -?> y) arr)+                    (a :: x) :: forall (z :: x). a :~: z ~> Type+type instance Apply (WhyCongPolySym arr x y f a :: a :~: z ~> Type) asdf+  = WhyCongPoly arr x y f a z asdf++cong :: forall (x :: Type) (y :: Type) (f :: x -> y)+               (a :: x) (b :: x).+        a :~: b+     -> f a :~: f b+cong = congPoly @(:->) @_ @_ @f++congTyFun :: forall (x :: Type) (y :: Type) (f :: x ~> y)+                    (a :: x) (b :: x).+             a :~: b+          -> f @@ a :~: f @@ b+congTyFun = congPoly @(:~>) @_ @_ @f++congPoly :: forall (arr :: FunArrow) (x :: Type) (y :: Type) (f :: (x -?> y) arr)+                   (a :: x) (b :: x).+            FunApp arr+         => a :~: b+         -> App x arr y f a :~: App x arr y f b+congPoly eq =+  withSomeSing eq $ \(singEq :: Sing r) ->+    (~>:~:) @x @a @b @r @(WhyCongPolySym arr x y f a) singEq Refl
+ tests/GADTSpec.hs view
@@ -0,0 +1,75 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+module GADTSpec where++import Data.Eliminator+import Data.Kind+import Data.Singletons++import Test.Hspec++main :: IO ()+main = hspec spec++spec :: Spec+spec = pure ()++-----++data So :: Bool -> Type where+  Oh :: So True++data instance Sing (z :: So what) where+  SOh :: Sing Oh++elimSo :: forall (what :: Bool) (s :: So what) (p :: forall (long_sucker :: Bool). So long_sucker -> Type).+          Sing s+       -> p Oh+       -> p s+elimSo SOh pOh = pOh++elimSoTyFun :: forall (what :: Bool) (s :: So what) (p :: forall (long_sucker :: Bool). So long_sucker ~> Type).+               Sing s+            -> p @@ Oh+            -> p @@ s+elimSoTyFun SOh pOh = pOh++{-+I don't know how to make this kind-check :(+elimSoPoly :: forall (arr :: FunArrow) (what :: Bool) (s :: So what)+                     (p :: forall (long_sucker :: Bool). (So long_sucker -?> Type) arr).+              Sing s+           -> App (So True) arr Type p Oh+           -> App (So what) arr Type p s+elimSoPoly SOh pOh = pOh+-}++data Obj :: Type where+  MkObj :: o -> Obj++data instance Sing (z :: Obj) where+  SMkObj :: forall (obj :: obiwan). Sing obj -> Sing (MkObj obj)++elimObj :: forall (o :: Obj) (p :: Obj -> Type).+           Sing o+        -> (forall (obj :: Type) (x :: obj). Sing x -> p (MkObj x))+        -> p o+elimObj = elimObjPoly @(:->) @o @p++elimObjTyFun :: forall (o :: Obj) (p :: Obj ~> Type).+                Sing o+             -> (forall (obj :: Type) (x :: obj). Sing x -> p @@ (MkObj x))+             -> p @@ o+elimObjTyFun = elimObjPoly @(:~>) @o @p++elimObjPoly :: forall (arr :: FunArrow) (o :: Obj) (p :: (Obj -?> Type) arr).+               Sing o+            -> (forall (obj :: Type) (x :: obj). Sing x -> App Obj arr Type p (MkObj x))+            -> App Obj arr Type p o+elimObjPoly (SMkObj (x :: Sing (obj :: obiwan))) pMkObj = pMkObj @obiwan @obj x
+ tests/ListSpec.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+module ListSpec where++import Data.Eliminator+import Data.Kind+import Data.Singletons.Prelude+import Data.Singletons.Prelude.List+import Data.Type.Equality++import EqualitySpec (congTyFun)++import ListTypes++import Test.Hspec++main :: IO ()+main = hspec spec++spec :: Spec+spec = pure ()++-----++mapPreservesLength :: forall (x :: Type) (y :: Type) (f :: x ~> y) (l :: [x]).+                      SingI l+                   => Length l :~: Length (Map f l)+mapPreservesLength+  = elimListTyFun @x @(WhyMapPreservesLengthSym1 f) @l (sing @_ @l) base step+  where+    base :: WhyMapPreservesLength f '[]+    base = Refl++    step :: forall (s :: x) (ss :: [x]).+            Sing s -> Sing ss+         -> WhyMapPreservesLength f ss+         -> WhyMapPreservesLength f (s:ss)+    step _ _ = congTyFun @_ @_ @((:+$$) 1)++mapFusion :: forall (x :: Type) (y :: Type) (z :: Type)+                    (f :: y ~> z) (g :: x ~> y) (l :: [x]).+                    SingI l+                 => Map f (Map g l) :~: Map (f :.$$$ g) l+mapFusion+  = elimListTyFun @x @(WhyMapFusionSym2 f g) @l (sing @_ @l) base step+  where+    base :: WhyMapFusion f g '[]+    base = Refl++    step :: forall (s :: x) (ss :: [x]).+            Sing s -> Sing ss+         -> WhyMapFusion f g ss+         -> WhyMapFusion f g (s:ss)+    step _ _ = congTyFun @_ @_ @((:$$) (f @@ (g @@ s)))
+ tests/ListTypes.hs view
@@ -0,0 +1,19 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+module ListTypes where++import Data.Singletons.Prelude+import Data.Singletons.Prelude.List+import Data.Singletons.TH++type WhyMapPreservesLength (f :: x ~> y) (l :: [x])+  = Length l :~: Length (Map f l)+$(genDefunSymbols [''WhyMapPreservesLength])++type WhyMapFusion (f :: y ~> z) (g :: x ~> y) (l :: [x])+  = Map f (Map g l) :~: Map (f :.$$$ g) l+$(genDefunSymbols [''WhyMapFusion])
+ tests/PeanoSpec.hs view
@@ -0,0 +1,116 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeInType #-}+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` VCons () VNil+  describe "mapVec" $ do+    it "maps over a Vec" $ do+      mapVec reverse ("hello" `VCons` "world" `VCons` VNil)+        `shouldBe` ("olleh" `VCons` "dlrow" `VCons` VNil)+  describe "zipWithVec" $ do+    it "zips two Vecs" $ do+      zipWithVec (,) ((2 :: Int) `VCons` 22 `VCons` VNil)+                     ("chicken-of-the-woods" `VCons` "hen-of-woods" `VCons` VNil)+        `shouldBe` ((2, "chicken-of-the-woods") `VCons` (22, "hen-of-woods")+                                                `VCons` VNil)+  describe "appendVec" $ do+    it "appends two Vecs" $ do+      appendVec ("portabello" `VCons` "bay-bolete"+                              `VCons` "funnel-chantrelle"+                              `VCons` VNil)+                ("sheathed-woodtuft" `VCons` "puffball" `VCons` VNil)+        `shouldBe` ("portabello" `VCons` "bay-bolete"+                                 `VCons` "funnel-chantrelle"+                                 `VCons` "sheathed-woodtuft"+                                 `VCons` "puffball"+                                 `VCons` VNil)+  describe "transposeVec" $ do+    it "transposes a Vec" $ do+      transposeVec (('a' `VCons` 'b' `VCons` 'c' `VCons` VNil)+            `VCons` ('d' `VCons` 'e' `VCons` 'f' `VCons` VNil)+            `VCons` VNil)+        `shouldBe`+                   (('a' `VCons` 'd' `VCons` VNil)+            `VCons` ('b' `VCons` 'e' `VCons` VNil)+            `VCons` ('c' `VCons` 'f' `VCons` VNil)+            `VCons` VNil)++-----++replicateVec :: forall (e :: Type) (howMany :: Peano).+                Sing howMany -> e -> Vec e howMany+replicateVec s e = elimPeano @howMany @(Vec e) s VNil step+  where+    step :: forall (k :: Peano). Sing k -> Vec e k -> Vec e (S k)+    step _ = VCons e++mapVec :: forall (a :: Type) (b :: Type) (n :: Peano).+          SingI n+       => (a -> b) -> Vec a n -> Vec b n+mapVec f = elimPeanoTyFun @n @(WhyMapVecSym2 a b) (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 = VCons (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 = elimPeanoTyFun @n @(WhyZipWithVecSym3 a b c) (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 = VCons (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 (Plus n m)+appendVec = elimPeanoTyFun @n @(WhyAppendVecSym2 e m) (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 = VCons (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 = elimPeanoTyFun @n @(WhyTransposeVecSym2 e m) (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 VCons (vhead vK) (transK (vtail vK))
+ tests/PeanoTypes.hs view
@@ -0,0 +1,124 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+module PeanoTypes where++import Data.Eliminator+import Data.Kind+import Data.Singletons.TH++$(singletons [d|+  data Peano = Z | S Peano++  plus :: Peano -> Peano -> Peano+  plus Z     m = m+  plus (S k) m = S (plus k m)++  times :: Peano -> Peano -> Peano+  times Z     _ = Z+  times (S k) m = plus m (times k m)+  |])++elimPeano :: forall (n :: Peano) (p :: Peano -> Type).+             Sing n+          -> p Z+          -> (forall (k :: Peano). Sing k -> p k -> p (S k))+          -> p n+elimPeano = elimPeanoPoly @(:->) @n @p++elimPeanoTyFun :: forall (n :: Peano) (p :: Peano ~> Type).+                  Sing n+               -> p @@ Z+               -> (forall (k :: Peano). Sing k -> p @@ k -> p @@ (S k))+               -> p @@ n+elimPeanoTyFun = elimPeanoPoly @(:~>) @n @p++elimPeanoPoly :: forall (arr :: FunArrow) (n :: Peano) (p :: (Peano -?> Type) arr).+                 FunApp arr+              => Sing n+              -> App Peano arr Type p Z+              -> (forall (k :: Peano). Sing k -> App Peano arr Type p k+                                              -> App Peano arr Type p (S k))+              -> App Peano arr Type p n+elimPeanoPoly SZ pZ _ = pZ+elimPeanoPoly (SS (sk :: Sing k)) pZ pS = pS sk (elimPeanoPoly @arr @k @p sk pZ pS)++data Vec a (n :: Peano) where+  VNil  :: Vec a Z+  VCons :: { vhead :: a, vtail :: Vec a n } -> Vec a (S n)+infixr 5 `VCons`+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+  SVCons :: { sVhead :: Sing x, sVtail :: Sing xs } -> Sing (VCons x xs)++instance SingKind a => SingKind (Vec a n) where+  type Demote (Vec a n) = Vec (Demote a) n+  fromSing SVNil         = VNil+  fromSing (SVCons x xs) = VCons (fromSing x) (fromSing xs)+  toSing VNil = SomeSing SVNil+  toSing (VCons x xs) =+    withSomeSing x $ \sx ->+      withSomeSing xs $ \sxs ->+        SomeSing $ SVCons sx sxs++instance SingI VNil where+  sing = SVNil++instance (SingI x, SingI xs) => SingI (VCons x xs) where+  sing = SVCons 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 (VCons x xs))+        -> p v+elimVec SVNil pVNil _ = pVNil+elimVec (SVCons sx (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =+  pVCons sx sxs (elimVec @a @k @p @xs sxs pVNil pVCons)++elimVecTyFun :: 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 @@ (VCons x xs))+             -> p @@ v+elimVecTyFun SVNil pVNil _ = pVNil+elimVecTyFun (SVCons sx (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =+  pVCons sx sxs (elimVecTyFun @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 (Plus n 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 (Times n 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
+ tests/Spec.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
+ tests/VecSpec.hs view
@@ -0,0 +1,43 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeInType #-}+module VecSpec where++import Data.Kind+import Data.Singletons++import PeanoSpec (appendVec)+import PeanoTypes++import Test.Hspec++main :: IO ()+main = hspec spec++spec :: Spec+spec = parallel $ do+  describe "concatVec" $ do+    it "concats a Vec of Vecs" $ do+      concatVec ((False `VCons` True  `VCons` False `VCons` VNil)+         `VCons` (True  `VCons` False `VCons` True  `VCons` VNil)+         `VCons` VNil)+        `shouldBe` (False `VCons` True  `VCons` False `VCons` True+                          `VCons` False `VCons` True  `VCons` VNil)++-----++concatVec :: forall (e :: Type) (n :: Peano) (j :: Peano).+             (SingKind e, SingI j, e ~ Demote e)+          => Vec (Vec e j) n -> Vec e (Times n j)+concatVec l = withSomeSing l $ \(singL :: Sing l) ->+                elimVecTyFun @(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).+                   Sing x -> Sing xs+                -> WhyConcatVec e j k     xs+                -> WhyConcatVec e j (S k) (VCons x xs)+    step h _ vKJ = appendVec (fromSing h) vKJ