packages feed

recursion-schemes-ix (empty) → 0.1.0.0

raw patch · 18 files changed

+1402/−0 lines, 18 filesdep +QuickCheckdep +basedep +containerssetup-changed

Dependencies added: QuickCheck, base, containers, hspec, mtl, recursion-schemes-ix, singlethongs

Files

+ ChangeLog.md view
@@ -0,0 +1,17 @@+# Changelog for recursion-schemes-ix++## 0.0.1.0++Initial release++Multiple last-minute changes:++* Switched from `singletons` to `singlethongs`+  - `singletons` has unnecessary dependencies, and is unable to compile+    with the current `ghcjs` version.+* Removed QuantifiedConstraints extension usage throughout+  - Allowed the removal of UndecidableInstances in most files+* Added the `ITraversable` class and monadic recursion-schemes+  - TODO: determine if `IFunctor` should just be removed,+    ie. determine if there are any `IFunctor`s that are not `ITraversable`+
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Skye Soss (c) 2020++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 Author name here 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,38 @@++# recursion-schemes-ix++## Recursion schemes over indexed datatypes++Heavily inspired by `multirec`, this library uses `PolyKinds`+and `SingI` constraints to achieve the same dependent typing as `multirec`.++This library defines the `IFunctor` typeclass and recursion-schemes+on `IFunctor`s.++Goals:+* Minimal dependencies+  - This library depends only on `singlethongs`, which in turn only depends+    on `template-haskell`. As a result, it should be easy to include in+    any project+* GHCJS compatibility+  - This package is used in a compiler that I want to be able to run in the+    browser+* Ease of use+  - Once everything is set-up, writing a recursion-scheme should not be+    overly complex (looking at you, `mulrirec`)++Non-Goals:+* Eliminating boilerplate+  - This library requires hand-written `IShow`, `IRead`, `IEq`, `IOrd`, `ITraversable` instances.+    I also recommend writing pattern synonyms to remove the `IFix` constructor.+    Writing these can be a pain, but its only required once for the main data structure,+    and one `IFunctor` instance whenever you write a dependent recursion-scheme.+* Speed+  - The code in the library mimics the `recurion-schemes` library almost directly,+    simply lifting everything up from `*` to `k -> *`. In a future release,+    `INLINE` pragmas will be added and possibly benchmarked.++## Documentation++Not written, but haddocks on the github user site.+
+ Setup.hs view
@@ -0,0 +1,2 @@+import           Distribution.Simple+main = defaultMain
+ recursion-schemes-ix.cabal view
@@ -0,0 +1,71 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: 20ec8e090059628c63cb93a58e4d0b51b601fbc74c1e66720dfae9482192e98b++name:           recursion-schemes-ix+version:        0.1.0.0+synopsis:       Recursion schemes over indexed Functors+description:    Please see the README on GitHub at <https://github.com/Skyb0rg007/recursion-schemes-ix#readme>+category:       Data+stability:      alpha+homepage:       https://github.com/Skyb0rg007/recursion-schemes-ix#readme+bug-reports:    https://github.com/Skyb0rg007/recursion-schemes-ix/issues+author:         Skye Soss+maintainer:     skyler.soss@gmail.com+copyright:      2020 Skye Soss+license:        BSD3+license-file:   LICENSE+tested-with:    GHC == 8.6.5 , GHC == 8.8.3 , GHC == 8.10.1 , GHCJS == 8.6.0.1+build-type:     Simple+extra-source-files:+    README.md+    ChangeLog.md++source-repository head+  type: git+  location: https://github.com/Skyb0rg007/recursion-schemes-ix++library+  exposed-modules:+      Data.IComonad+      Data.IFunction+      Data.IFunctor+      Data.IFunctor.Classes+      Data.IFunctor.Foldable+      Data.IFunctor.ICofree+      Data.IFunctor.IFree+      Data.IFunctor.IIdentity+      Data.IMonad+      Data.ITraversable+  other-modules:+      Paths_recursion_schemes_ix+  hs-source-dirs:+      src+  build-depends:+      base >=4.12 && <4.15+    , singlethongs ==0.1+  default-language: Haskell2010++test-suite recursion-schemes-ix-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  other-modules:+      FibSpec+      GRINSpec+      Paths_recursion_schemes_ix+  hs-source-dirs:+      test+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      QuickCheck+    , base >=4.12 && <4.15+    , containers+    , hspec+    , mtl+    , recursion-schemes-ix+    , singlethongs ==0.1+  default-language: Haskell2010
+ src/Data/IComonad.hs view
@@ -0,0 +1,28 @@+{-# LANGUAGE PolyKinds     #-}+{-# LANGUAGE RankNTypes    #-}+{-# LANGUAGE TypeOperators #-}++{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}++module Data.IComonad+    ( IComonad (..)+    -- * Re-exports+    , module Data.IFunctor+    ) where++import           Data.Functor.Product (Product (Pair))+import           Data.IFunctor        (IFunctor (imap), type (~~>))++-- | Comonoid in the category of dependent endofunctors+class IFunctor f => IComonad f where+    iextract :: f a ~~> a+    iduplicate :: f a ~~> f (f a)+    iduplicate = iextend id+    iextend :: (f a ~~> b) -> (f a ~~> f b)+    iextend f = imap f . iduplicate+    {-# MINIMAL iextract, (iduplicate | iextend) #-}++instance IComonad (Product a) where+    iextract (Pair _ b) = b+    iduplicate (Pair a b) = Pair a (Pair a b)+
+ src/Data/IFunction.hs view
@@ -0,0 +1,17 @@+{-# LANGUAGE PolyKinds     #-}+{-# LANGUAGE RankNTypes    #-}+{-# LANGUAGE TypeOperators #-}++{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}++module Data.IFunction+    ( type (~~>)+    ) where++import           Singlethongs (SingI)++infixr 4 ~~>++-- | Indexed function type+type a ~~> b = forall ix. SingI ix => a ix -> b ix+
+ src/Data/IFunctor.hs view
@@ -0,0 +1,27 @@+{-# LANGUAGE PolyKinds     #-}+{-# LANGUAGE RankNTypes    #-}+{-# LANGUAGE TypeOperators #-}++{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}++module Data.IFunctor+    ( IFunctor (..)+    -- * Re-exports+    , module Data.IFunction+    ) where++import           Data.Functor.Product (Product (Pair))+import           Data.Functor.Sum     (Sum (InL, InR))+import           Data.IFunction       (type (~~>))++-- | Functor in the category of dependent types+class IFunctor f where+    imap :: (a ~~> b) -> (f a ~~> f b)++instance IFunctor (Sum a) where+    imap _ (InL x) = InL x+    imap f (InR x) = InR (f x)++instance IFunctor (Product a) where+    imap f (Pair a b) = Pair a (f b)+
+ src/Data/IFunctor/Classes.hs view
@@ -0,0 +1,142 @@+{-# LANGUAGE PolyKinds  #-}+{-# LANGUAGE RankNTypes #-}++{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}++module Data.IFunctor.Classes+    (+    -- * Indexed Show+      IShow (..)+    , IShow2 (..)+    , ishowsPrec1+    , ishow1+    -- * Indexed Read+    , IRead (..)+    , IRead2 (..)+    , ireadPrec1+    , ireadsPrec1+    -- * Indexed Eq+    , IEq (..)+    , IEq2 (..)+    , ieq1+    -- * Indexed Ord+    , IOrd (..)+    , IOrd2 (..)+    , icompare1+    ) where++import           Data.Functor.Product (Product (..))+import           Data.Functor.Sum     (Sum (..))+import           Singlethongs         (SingI)+import           Text.Read++class IShow f where+    ishowsPrec :: SingI ix => (forall ix. SingI ix => Int -> a ix -> ShowS) -> Int -> f a ix -> ShowS+    ishowsPrec sp _ x s = ishow sp x ++ s+    ishow :: SingI ix => (forall ix. SingI ix => Int -> a ix -> ShowS) -> f a ix -> String+    ishow sp x = ishowsPrec sp 0 x ""+    {-# MINIMAL ishowsPrec | ishow #-}++class IShow2 a where+    ishowsPrec2 :: SingI ix => Int -> a ix -> ShowS+    ishowsPrec2 _ x s = ishow2 x ++ s+    ishow2 :: SingI ix => a ix -> String+    ishow2 x = ishowsPrec2 0 x ""+    {-# MINIMAL ishowsPrec2 | ishow2 #-}++ishowsPrec1 :: (IShow f, IShow2 a, SingI ix) => Int -> f a ix -> ShowS+ishowsPrec1 = ishowsPrec ishowsPrec2++ishow1 :: (IShow f, IShow2 a, SingI ix) => f a ix -> String+ishow1 = ishow ishowsPrec2++class IRead f where+    ireadPrec :: SingI ix => (forall ix. SingI ix => ReadPrec (a ix)) -> ReadPrec (f a ix)+    ireadPrec rp = readS_to_Prec $ ireadsPrec (readPrec_to_S rp)+    ireadsPrec :: SingI ix => (forall ix. SingI ix => Int -> ReadS (a ix)) -> Int -> ReadS (f a ix)+    ireadsPrec rp = readPrec_to_S $ ireadPrec (readS_to_Prec rp)+    {-# MINIMAL ireadPrec | ireadsPrec #-}++class IRead2 a where+    ireadPrec2 :: SingI ix => ReadPrec (a ix)+    ireadPrec2 = readS_to_Prec $ ireadsPrec2+    ireadsPrec2 :: SingI ix => Int -> ReadS (a ix)+    ireadsPrec2 = readPrec_to_S $ ireadPrec2+    {-# MINIMAL ireadPrec2 | ireadsPrec2 #-}++ireadPrec1 :: (IRead f, IRead2 a, SingI ix) => ReadPrec (f a ix)+ireadPrec1 = ireadPrec ireadPrec2++ireadsPrec1 :: (IRead f, IRead2 a, SingI ix) => Int -> ReadS (f a ix)+ireadsPrec1 = ireadsPrec ireadsPrec2++class IEq f where+    ieq :: SingI ix => (forall ix. SingI ix => a ix -> a ix -> Bool) -> f a ix -> f a ix -> Bool++class IEq2 a where+    ieq2 :: SingI ix => a ix -> a ix -> Bool++ieq1 :: (IEq f, IEq2 a, SingI ix) => f a ix -> f a ix -> Bool+ieq1 = ieq ieq2++class IEq f => IOrd f where+    icompare :: SingI ix => (forall ix. SingI ix => a ix -> a ix -> Ordering) -> f a ix -> f a ix -> Ordering++class IEq2 a => IOrd2 a where+    icompare2 :: SingI ix => a ix -> a ix -> Ordering++icompare1 :: (IOrd f, IOrd2 a, SingI ix) => f a ix -> f a ix -> Ordering+icompare1 = icompare icompare2++-- * base instances++-- Sum+instance IShow2 a => IShow (Sum a) where+    ishowsPrec _ p (InL x) = showParen (p > 10) $+        showString "InL " . ishowsPrec2 11 x+    ishowsPrec sp p (InR x) = showParen (p > 10) $+        showString "InR " . sp 11 x++instance IRead2 a => IRead (Sum a) where+    ireadPrec rp = parens $+        (prec 10 $ do+            Ident "InL" <- lexP+            x <- step ireadPrec2+            pure $ InL x+        )+        ++++        (prec 10 $ do+            Ident "InR" <- lexP+            x <- step rp+            pure $ InR x+        )++instance IEq2 a => IEq (Sum a) where+    ieq _  (InL x) (InL y) = ieq2 x y+    ieq eq (InR x) (InR y) = eq x y+    ieq _ _ _              = False++instance IOrd2 a => IOrd (Sum a) where+    icompare _ (InL x) (InL y)    = icompare2 x y+    icompare comp (InR x) (InR y) = comp x y+    icompare _ (InL _) (InR _)    = LT+    icompare _ (InR _) (InL _)    = GT++-- Product+instance IShow2 a => IShow (Product a) where+    ishowsPrec sp p (Pair a b) = showParen (p > 10) $+        showString "Pair " . ishowsPrec2 11 a . showString " " . sp 11 b++instance IRead2 a => IRead (Product a) where+    ireadPrec rp = parens $ prec 10 $ do+        Ident "Pair" <- lexP+        x <- step ireadPrec2+        y <- step rp+        pure $ Pair x y++instance IEq2 a => IEq (Product a) where+    ieq eq (Pair a b) (Pair a' b') = ieq2 a a' && eq b b'++instance IOrd2 a => IOrd (Product a) where+    icompare comp (Pair a b) (Pair a' b') = icompare2 a a' <> comp b b'+
+ src/Data/IFunctor/Foldable.hs view
@@ -0,0 +1,408 @@+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE DeriveDataTypeable   #-}+{-# LANGUAGE DeriveGeneric        #-}+{-# LANGUAGE LambdaCase           #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE RankNTypes           #-}+{-# LANGUAGE ScopedTypeVariables  #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}++{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}++module Data.IFunctor.Foldable+    (+    -- * Fixpoint for indexed types+      IFix (..)+    -- * Morphisms+    -- * Constructive morphisms+    , cata+    , prepro+    , para+    , zygo+    , histo+    -- * Destructive morphisms+    , ana+    , postpro+    , apo+    , gapo+    , futu+    -- * Combined morphisms+    , hylo+    , dyna+    , chrono+    , meta+    , elgot+    , coelgot+    -- * Monadic morphisms+    , cataM+    , paraM+    , anaM+    , apoM+    , hyloM+    , dynaM+    -- * Distribution Laws+    , DistLaw+    -- * Constructive distribution laws+    , distCata+    , distPara+    , distZygo+    , distHisto+    -- * Destructive distribution laws+    , distAna+    , distApo+    , distGApo+    , distFutu+    -- * Generalized morphisms+    , gfold+    , gunfold+    , ghylo+    , gprepro+    , gpostpro+    -- * Generalized monadic morphisms+    , gfoldM+    , gunfoldM+    , ghyloM+    -- * Re-exports+    , module Data.Functor.Const+    , module Data.Functor.Product+    , module Data.Functor.Sum+    , module Data.IComonad+    , module Data.IFunction+    , module Data.IFunctor+    , module Data.IFunctor.Classes+    , module Data.IFunctor.ICofree+    , module Data.IFunctor.IFree+    , module Data.IFunctor.IIdentity+    , module Data.IMonad+    , module Data.ITraversable+    , module Singlethongs+    ) where++import           Control.Monad           ((<=<))+import           Data.Functor.Const      (Const (..))+import           Data.Functor.Product    (Product (..))+import           Data.Functor.Sum        (Sum (..))+import           Data.IComonad           (IComonad (..))+import           Data.IFunction          (type (~~>))+import           Data.IFunctor           (IFunctor (..))+import           Data.IFunctor.Classes+import           Data.IFunctor.ICofree   (ICofree (..))+import           Data.IFunctor.IFree     (IFree (..))+import           Data.IFunctor.IIdentity (IIdentity (..))+import           Data.IMonad             (IMonad (..))+import           Data.ITraversable       (ITraversable (..), imapDefault)+import           Data.Typeable           (Typeable)+import           GHC.Generics            (Generic, Generic1)+import           Singlethongs            (SingI (sing))+import           Text.Read++-- | Fixpoint type+newtype IFix f ix = IFix { unIFix :: f (IFix f) ix }+    deriving (Typeable, Generic, Generic1)++instance (IShow f, SingI ix) => Show (IFix f ix) where+    showsPrec p (IFix x) = showParen (p > 10) $+        showString "IFix " .  ishowsPrec showsPrec 11 x++instance (IRead f, SingI ix) => Read (IFix f ix) where+    readPrec = parens $ prec 10 $ do+        Ident "IFix" <- lexP+        x <- step $ ireadPrec readPrec+        pure $ IFix x++instance (IEq f, SingI ix) => Eq (IFix f ix) where+    IFix x == IFix y = ieq (==) x y++instance (IOrd f, SingI ix) => Ord (IFix f ix) where+    IFix x `compare` IFix y = icompare compare x y++-- * Morphisms++-- | Catamorphism, ie. fold+cata :: IFunctor f+     => (f a ~~> a)+     -> (IFix f ~~> a)+cata f = gfold distCata (f . imap runIIdentity)++-- | Fokkinga's prepromorphism+prepro :: IFunctor f+       => (forall b. f b ~~> f b)+       -> (f a ~~> a)+       -> (IFix f ~~> a)+prepro e f = gprepro distCata e (f . imap runIIdentity)++-- | Paramorphism+para :: IFunctor f+     => (f (Product (IFix f) a) ~~> a)+     -> (IFix f ~~> a)+para = gfold distPara++-- | Zygomorphism+zygo :: IFunctor f+     => (f b ~~> b)+     -> (f (Product b a) ~~> a)+     -> (IFix f ~~> a)+zygo f = gfold (distZygo f)++-- | Histomorphism+histo :: IFunctor f+      => (f (ICofree f a) ~~> a)+      -> (IFix f ~~> a)+histo = gfold distHisto++-- | Anamorphism, ie. unfold+ana :: IFunctor f+    => (a ~~> f a)+    -> (a ~~> IFix f)+ana g = gunfold distAna (imap IIdentity . g)++-- | Fokkinga's postpromorphism+postpro :: IFunctor f+        => (forall b. f b ~~> f b)+        -> (a ~~> f a)+        -> (a ~~> IFix f)+postpro e g = gpostpro distAna e (imap IIdentity . g)++-- | Apomorphism+apo :: IFunctor f+    => (a ~~> f (Sum (IFix f) a))+    -> (a ~~> IFix f)+apo = gunfold distApo++-- | GApomorphism+gapo :: IFunctor f+     => (b ~~> f b)+     -> (a ~~> f (Sum b a))+     -> (a ~~> IFix f)+gapo f = gunfold (distGApo f)++-- | Futumorphism+futu :: IFunctor f+     => (a ~~> f (IFree f a))+     -> (a ~~> IFix f)+futu = gunfold distFutu++-- | Hylomorphism, fold then unfold+hylo :: IFunctor f+     => (f b ~~> b)+     -> (a ~~> f a)+     -> (a ~~> b)+hylo f g = ghylo distCata distAna (f . imap runIIdentity) (imap IIdentity . g)++-- | Dynamorphism+dyna :: IFunctor f+     => (f (ICofree f b) ~~> b)+     -> (a ~~> f a)+     -> (a ~~> b)+dyna f g = ghylo distHisto distAna f (imap IIdentity . g)++-- | Chronomorphism+chrono :: IFunctor f+       => (f (ICofree f b) ~~> b)+       -> (a ~~> f (IFree f a))+       -> (a ~~> b)+chrono = ghylo distHisto distFutu++-- | Metamorphism+-- TODO: ensure only 1 pass over structure+meta :: (IFunctor f, IFunctor g)+     => (f a ~~> a)+     -> (a ~~> b)+     -> (b ~~> g b)+     -> (IFix f ~~> IFix g)+meta f e g = ana g . e . cata f++-- * Elgot algebras++elgot :: forall f a b. IFunctor f+      => (f a ~~> a)+      -> (b ~~> Sum a (f b))+      -> (b ~~> a)+elgot phi psi = h+    where+        h :: b ~~> a+        h = (id `sum` (phi . imap h)) . psi+        sum :: forall a b c. (a ~~> c) -> (b ~~> c) -> (Sum a b ~~> c)+        sum f _ (InL x) = f x+        sum _ g (InR x) = g x++coelgot :: forall f a b. IFunctor f+        => (Product a (f b) ~~> b)+        -> (a ~~> f a)+        -> (a ~~> b)+coelgot phi psi = h+    where+        h :: a ~~> b+        h = phi . (id `product` (imap h . psi))+        product :: forall a b c. (a ~~> b) -> (a ~~> c) -> (a ~~> Product b c)+        product f g x = Pair (f x) (g x)+++-- * Monadic morphisms++-- | Monadic catamorphism+cataM :: (ITraversable f, Monad m)+      => (forall ix. SingI ix => f a ix -> m (a ix))+      -> (forall ix. SingI ix => IFix f ix -> m (a ix))+cataM f = gfoldM distCata (f . imap runIIdentity)++-- | Monadic Paramorphism+paraM :: (ITraversable f, Monad m)+      => (forall ix. SingI ix => f (Product (IFix f) a) ix -> m (a ix))+      -> (forall ix. SingI ix => IFix f ix -> m (a ix))+paraM = gfoldM distPara++-- | Monadic anamorphism+anaM :: (ITraversable f, Monad m)+     => (forall ix. SingI ix => a ix -> m (f a ix))+     -> (forall ix. SingI ix => a ix -> m (IFix f ix))+anaM g = gunfoldM distAna (fmap (imap IIdentity) . g)++-- | Monadic apomorphism+apoM :: (ITraversable f, Monad m)+     => (forall ix. SingI ix => a ix -> m (f (Sum (IFix f) a) ix))+     -> (forall ix. SingI ix => a ix -> m (IFix f ix))+apoM = gunfoldM distApo++-- | Monadic hylomorphism+hyloM :: (ITraversable f, Monad m)+     => (forall ix. SingI ix => f b ix -> m (b ix))+     -> (forall ix. SingI ix => a ix -> m (f a ix))+     -> (forall ix. SingI ix => a ix -> m (b ix))+hyloM f g = ghyloM distCata distAna (f . imap runIIdentity) (fmap (imap IIdentity) . g)++-- | Monadic dynamorphism+dynaM :: (ITraversable f, Monad m)+      => (forall ix. SingI ix => f (ICofree f b) ix -> m (b ix))+      -> (forall ix. SingI ix => a ix -> m (f a ix))+      -> (forall ix. SingI ix => a ix -> m (b ix))+dynaM f g = ghyloM distHisto distAna f (fmap (imap IIdentity) . g)++-- * Distribution laws++-- | Type of distribution laws+-- A Constructive morphism means the second part is a 'IComonad'+-- A Destructive morphism means the first part is an 'IMonad'+type DistLaw f g = forall a. f (g a) ~~> g (f a)++-- * Constructive distribution laws++distCata :: IFunctor f => DistLaw f IIdentity+distCata = IIdentity . imap runIIdentity++distPara :: IFunctor f => DistLaw f (Product (IFix f))+distPara = distZygo IFix++distZygo :: IFunctor f => (f b ~~> b) -> DistLaw f (Product b)+distZygo g m = Pair (g (imap (\(Pair a _) -> a) m)) (imap (\(Pair _ b) -> b) m)++distHisto :: IFunctor f => DistLaw f (ICofree f)+distHisto x = imap (\(a ::< _) -> a) x ::< imap (\(_ ::< x) -> distHisto x) x++-- * Destructive distribution laws++distAna :: IFunctor f => DistLaw IIdentity f+distAna = imap IIdentity . runIIdentity++distApo :: IFunctor f => DistLaw (Sum (IFix f)) f+distApo = distGApo unIFix++distGApo :: IFunctor f => (b ~~> f b) -> DistLaw (Sum b) f+distGApo f (InL x) = imap InL $ f x+distGApo _ (InR x) = imap InR x++distFutu :: IFunctor f => DistLaw (IFree f) f+distFutu (IPure x) = imap IPure x+distFutu (IFree x) = imap (IFree . distFutu) x++-- * Generalized combinators++-- | Generalized fold+gfold :: forall f w a. (IFunctor f, IComonad w)+      => DistLaw f w+      -> (f (w a) ~~> a)+      -> (IFix f ~~> a)+gfold k g = g . iextract . c+    where+        c :: IFix f ~~> w (f (w a))+        c = k . imap (iduplicate . imap g . c) . unIFix++-- | Generalized unfold+gunfold :: forall f m a. (IFunctor f, IMonad m)+        => DistLaw m f+        -> (a ~~> f (m a))+        -> (a ~~> IFix f)+gunfold k f = a . ipure . f+    where+        a :: m (f (m a)) ~~> IFix f+        a = IFix . imap (a . imap f . ijoin) . k++-- | Generalized hylomorphism+ghylo :: forall f w m a b. (IFunctor f, IComonad w, IMonad m)+      => DistLaw f w+      -> DistLaw m f+      -> f (w b) ~~> b+      -> a ~~> f (m a)+      -> a ~~> b+ghylo w m f g = iextract . h . ipure+    where+        h :: m a ~~> w b+        h = imap f . w . imap (iduplicate . h . ijoin) . m . imap g++-- | Generalized monadic fold+gfoldM :: forall f w m a. (ITraversable f, ITraversable w, IComonad w, Monad m)+       => DistLaw f w+       -> (forall ix. SingI ix => f (w a) ix -> m (a ix))+       -> (forall ix. SingI ix => IFix f ix -> m (a ix))+gfoldM k g = g . iextract <=< c+    where+        c :: forall ix. SingI ix => IFix f ix -> m (w (f (w a)) ix)+        c = fmap k . itraverse (fmap iduplicate . itraverse g <=< c) . unIFix++-- | Generalized monadic unfold+gunfoldM :: forall f m a x. (ITraversable f, ITraversable m, IMonad m, Monad x)+         => DistLaw m f+         -> (forall ix. SingI ix => a ix -> x (f (m a) ix))+         -> (forall ix. SingI ix => a ix -> x (IFix f ix))+gunfoldM k f = a . ipure <=< f+    where+        a :: SingI ix => m (f (m a)) ix -> x (IFix f ix)+        a = fmap IFix . itraverse (a <=< itraverse f . ijoin) . k++-- | Generalized monadic hylomorphism+ghyloM :: forall f w m a b x. (ITraversable f, ITraversable w, ITraversable m, IComonad w, IMonad m, Monad x)+       => DistLaw f w+       -> DistLaw m f+       -> (forall ix. SingI ix => f (w b) ix -> x (b ix))+       -> (forall ix. SingI ix => a ix -> x (f (m a) ix))+       -> (forall ix. SingI ix => a ix -> x (b ix))+ghyloM w m f g = fmap iextract . h . ipure+    where+        h :: SingI ix => m a ix -> x (w b ix)+        h = itraverse f <=< fmap w . itraverse (fmap iduplicate . h . ijoin) . m <=< itraverse g++-- | Generalized prepromorphism+gprepro :: forall f w a. (IFunctor f, IComonad w)+        => DistLaw f w+        -> (forall c. f c ~~> f c)+        -> (f (w a) ~~> a)+        -> (IFix f ~~> a)+gprepro k e f = iextract . c+    where+        c :: IFix f ~~> w a+        c = imap f . k . imap (iduplicate . c . cata (IFix . e)) . unIFix++-- | Generalized postpromorphism+gpostpro :: forall f m a. (IFunctor f, IMonad m)+         => DistLaw m f+         -> (forall c. f c ~~> f c)+         -> (a ~~> f (m a))+         -> (a ~~> IFix f)+gpostpro k e g = a . ipure+    where+        a :: m a ~~> IFix f+        a = IFix . imap (cata (IFix . e) . a . ijoin) . k . imap g+++
+ src/Data/IFunctor/ICofree.hs view
@@ -0,0 +1,68 @@+{-# LANGUAGE DeriveDataTypeable    #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-}++{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}++module Data.IFunctor.ICofree+    ( ICofree (..)+    ) where++import           Data.IComonad         (IComonad (..))+import           Data.IFunctor         (IFunctor (..))+import           Data.IFunctor.Classes+import           Data.ITraversable     (ITraversable (..))+import           Data.Typeable         (Typeable)+import           GHC.Generics          (Generic, Generic1)+import           Singlethongs          (SingI)+import           Text.Read++infixr 5 ::<++-- | Cofree IComonad+data ICofree f a ix = a ix ::< f (ICofree f a) ix+    deriving (Typeable, Generic, Generic1)++instance IFunctor f => IFunctor (ICofree f) where+    imap f (a ::< x) = f a ::< imap (imap f) x++instance ITraversable f => ITraversable (ICofree f) where+    itraverse f (a ::< x) = (::<) <$> f a <*> itraverse (itraverse f) x++instance IFunctor f => IComonad (ICofree f) where+    iextract (a ::< _) = a+    iduplicate (a ::< x) = (a ::< x) ::< imap iduplicate x+    iextend f (a ::< x) = f (a ::< x) ::< imap (iextend f) x++instance IShow f => IShow (ICofree f) where+    ishowsPrec sp p (a ::< x) = showParen (p > 5) $+        sp 6 a . showString " ::< " . ishowsPrec (ishowsPrec sp) 6 x++instance IRead f => IRead (ICofree f) where+    ireadPrec rp = parens $ prec 5 $ do+        a <- step rp+        Symbol "::<" <- lexP+        x <- step (ireadPrec (ireadPrec rp))+        pure (a ::< x)++instance IEq f => IEq (ICofree f) where+    ieq eq (a ::< x) (a' ::< x') = eq a a' && ieq (ieq eq) x x'++instance IOrd f => IOrd (ICofree f) where+    icompare comp (a ::< x) (a' ::< x') = comp a a' <> icompare (icompare comp) x x'++instance (IShow f, IShow2 a, SingI ix) => Show (ICofree f a ix) where+    showsPrec = ishowsPrec1++instance (IRead f, IRead2 a, SingI ix) => Read (ICofree f a ix) where+    readPrec = ireadPrec1++instance (IEq f, IEq2 a, SingI ix) => Eq (ICofree f a ix) where+    (==) = ieq1++instance (IOrd f, IOrd2 a, SingI ix) => Ord (ICofree f a ix) where+    compare = icompare1
+ src/Data/IFunctor/IFree.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE DeriveDataTypeable    #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-}++{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}++module Data.IFunctor.IFree+    ( IFree (..)+    ) where++import           Data.IFunctor         (IFunctor (..))+import           Data.IFunctor.Classes+import           Data.IMonad           (IMonad (..))+import           Data.ITraversable     (ITraversable (..))+import           Data.Typeable         (Typeable)+import           GHC.Generics          (Generic, Generic1)+import           Singlethongs          (SingI)+import           Text.Read++-- | Free IMonad+data IFree f a ix = IPure (a ix)+    | IFree (f (IFree f a) ix)+    deriving (Typeable, Generic, Generic1)++instance IFunctor f => IFunctor (IFree f) where+    imap f (IPure x) = IPure (f x)+    imap f (IFree x) = IFree (imap (imap f) x)++instance ITraversable f => ITraversable (IFree f) where+    itraverse f (IPure x) = IPure <$> f x+    itraverse f (IFree x) = IFree <$> itraverse (itraverse f) x++instance IFunctor f => IMonad (IFree f) where+    ipure = IPure+    ijoin (IPure x) = x+    ijoin (IFree x) = IFree $ imap ijoin x+    ibind f (IPure x) = f x+    ibind f (IFree x) = IFree $ imap (ibind f) x++instance IShow f => IShow (IFree f) where+    ishowsPrec sp p (IPure x) = showParen (p > 10) $+        showString "IPure " . sp 11 x+    ishowsPrec sp p (IFree x) = showParen (p > 10) $+        showString "IFree " . (ishowsPrec (ishowsPrec sp)) 11 x++instance IRead f => IRead (IFree f) where+    ireadPrec rp = parens $+        (prec 10 $ do+            Ident "IPure" <- lexP+            x <- step rp+            pure $ IPure x+        )+        ++++        (prec 10 $ do+            Ident "IFree" <- lexP+            x <- step (ireadPrec (ireadPrec rp))+            pure $ IFree x+        )++instance IEq f => IEq (IFree f) where+    ieq eq (IPure x) (IPure y) = eq x y+    ieq eq (IFree x) (IFree y) = ieq (ieq eq) x y+    ieq _ _ _                  = False++instance IOrd f => IOrd (IFree f) where+    icompare comp (IPure x) (IPure y) = comp x y+    icompare comp (IFree x) (IFree y) = icompare (icompare comp) x y+    icompare _ (IPure _) (IFree _)    = LT+    icompare _ (IFree _) (IPure _)    = GT++instance (IShow f, IShow2 a, SingI ix) => Show (IFree f a ix) where+    showsPrec = ishowsPrec1++instance (IRead f, IRead2 a, SingI ix) => Read (IFree f a ix) where+    readPrec = ireadPrec1++instance (IEq f, IEq2 a, SingI ix) => Eq (IFree f a ix) where+    (==) = ieq1++instance (IOrd f, IOrd2 a, SingI ix) => Ord (IFree f a ix) where+    compare = icompare1++
+ src/Data/IFunctor/IIdentity.hs view
@@ -0,0 +1,72 @@+{-# LANGUAGE DeriveDataTypeable    #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE TypeOperators         #-}++{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}++module Data.IFunctor.IIdentity+    ( IIdentity (IIdentity, runIIdentity)+    ) where++import           Data.Data             (Data)+import           Data.Function         (on)+import           Data.IComonad         (IComonad (..))+import           Data.IFunctor         (IFunctor (..))+import           Data.IFunctor.Classes+import           Data.IMonad           (IMonad (..))+import           Data.ITraversable     (ITraversable (..))+import           Data.Typeable         (Typeable)+import           GHC.Generics          (Generic, Generic1)+import           Singlethongs          (SingI)+import           Text.Read++data IIdentity f ix = IIdentity+    { runIIdentity :: f ix+    }+    deriving (Typeable, Data, Generic, Generic1)++instance IFunctor IIdentity where+    imap f = IIdentity . f . runIIdentity++instance IMonad IIdentity where+    ipure = IIdentity+    ijoin = runIIdentity++instance IComonad IIdentity where+    iextract = runIIdentity+    iduplicate = IIdentity++instance ITraversable IIdentity where+    itraverse f = fmap IIdentity . f . runIIdentity++instance IShow IIdentity where+    ishowsPrec sp p (IIdentity x) = showParen (p > 10) $+        showString "IIdentity " . sp p x++instance IRead IIdentity where+    ireadPrec rp = parens $ prec 10 $ do+        Ident "IIdentity" <- lexP+        x <- step rp+        pure $ IIdentity x++instance IEq IIdentity where+    ieq eq = eq `on` runIIdentity++instance IOrd IIdentity where+    icompare comp = comp `on` runIIdentity++instance (IShow2 f, SingI ix) => Show (IIdentity f ix) where+    showsPrec = ishowsPrec1++instance (IRead2 f, SingI ix) => Read (IIdentity f ix) where+    readPrec = ireadPrec1++instance (IEq2 f, SingI ix) => Eq (IIdentity f ix) where+    (==) = ieq1++instance (IOrd2 f, SingI ix) => Ord (IIdentity f ix) where+    compare = icompare1+
+ src/Data/IMonad.hs view
@@ -0,0 +1,28 @@+{-# LANGUAGE PolyKinds     #-}+{-# LANGUAGE RankNTypes    #-}+{-# LANGUAGE TypeOperators #-}++{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}++module Data.IMonad+    ( IMonad (..)+    -- * Re-exports+    , module Data.IFunctor+    ) where++import           Data.Functor.Sum (Sum (InL, InR))+import           Data.IFunctor    (IFunctor (imap), type (~~>))++class IFunctor f => IMonad f where+    ipure :: a ~~> f a+    ijoin :: f (f a) ~~> f a+    ijoin = ibind id+    ibind :: (a ~~> f b) -> (f a ~~> f b)+    ibind f = ijoin . imap f+    {-# MINIMAL ipure, (ijoin | ibind) #-}++instance IMonad (Sum a) where+    ipure = InR+    ijoin (InL x) = InL x+    ijoin (InR x) = x+
+ src/Data/ITraversable.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE PolyKinds     #-}+{-# LANGUAGE RankNTypes    #-}+{-# LANGUAGE TypeOperators #-}++{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}++module Data.ITraversable+    ( ITraversable (..)+    , imapDefault+    -- * Re-exports+    , module Data.IFunctor+    ) where++import           Data.Functor.Identity (Identity (Identity, runIdentity))+import           Data.Functor.Product  (Product (Pair))+import           Data.Functor.Sum      (Sum (InL, InR))+import           Data.IFunctor+import           Singlethongs          (SingI)++class IFunctor f => ITraversable f where+    itraverse :: (Applicative m, SingI ix)+              => (forall ix. SingI ix => a ix -> m (b ix))+              -> f a ix+              -> m (f b ix)++-- | Default 'imap' for deriving 'IFunctor'+imapDefault :: ITraversable f+            => (a ~~> b)+            -> (f a ~~> f b)+imapDefault f = runIdentity . itraverse (Identity . f)++instance ITraversable (Sum a) where+    itraverse _ (InL x) = pure $ InL x+    itraverse f (InR x) = InR <$> f x++instance ITraversable (Product a) where+    itraverse f (Pair a b) = Pair a <$> f b+
+ test/FibSpec.hs view
@@ -0,0 +1,71 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DeriveDataTypeable    #-}+{-# LANGUAGE DeriveGeneric         #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE InstanceSigs          #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE LambdaCase            #-}+{-# LANGUAGE NoStarIsType          #-}+{-# LANGUAGE PatternSynonyms       #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE TemplateHaskell       #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}++module FibSpec (main, spec) where++import           Data.IFunctor.Foldable+import           Data.Kind               (Type)+import           Singlethongs+import           Test.Hspec+import           Test.QuickCheck++data PeanoIdx = PeanoIdx+singlethongs ''PeanoIdx++main :: IO ()+main = hspec spec++spec :: Spec+spec =+    describe "fib using 'dyna'" $ do+        it "fibs" $+            map fib [1 .. 8]+            `shouldBe`+            [1, 1, 2, 3, 5, 8, 13, 21]++fib :: Integer -> Integer+fib = getConst . fib' . Const+    where+        fib' :: Const Integer 'PeanoIdx -> Const Integer 'PeanoIdx+        fib' = dyna folder builder+        folder :: forall ix. SingI ix+               => PeanoF (ICofree PeanoF (Const Integer)) ix+               -> Const Integer ix+        folder OneF                            = 1+        folder (SuccF (_ ::< OneF))            = 1+        folder (SuccF (a ::< SuccF (b ::< _))) = a + b+        builder :: forall ix. SingI ix+                => Const Integer ix+                -> PeanoF (Const Integer) ix+        builder n =+          case sing :: Sing ix of+            SPeanoIdx ->+              if n <= 1+                then OneF+                else SuccF (n - 1)++data PeanoF f ix where+    OneF  :: PeanoF f 'PeanoIdx+    SuccF :: f 'PeanoIdx -> PeanoF f 'PeanoIdx++instance IFunctor PeanoF where+    imap _ OneF      = OneF+    imap f (SuccF x) = SuccF (f x)++
+ test/GRINSpec.hs view
@@ -0,0 +1,243 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE InstanceSigs        #-}+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE PolyKinds           #-}+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell     #-}+{-# LANGUAGE TypeApplications    #-}+{-# LANGUAGE TypeFamilies        #-}+{-# LANGUAGE TypeOperators       #-}++module GRINSpec (main, spec) where++import           Control.Monad.State+import           Data.IFunctor.Foldable+import           Data.Map               (Map)+import qualified Data.Map               as Map+import           Data.Set               (Set)+import qualified Data.Set               as Set+import           Singlethongs+import           Test.Hspec+import           Test.QuickCheck+import           Text.Show              (showListWith)++data ASTIdx = Exp | SimpleExp | Alt | Program | Def+singlethongs ''ASTIdx++main :: IO ()+main = hspec spec++spec :: Spec+spec = do+    describe "lorem ipsum" $ do+        it "asdf" $+            1 `shouldBe` 1+    describe "Show instance for IFix" $ do+        it "is correct" $+            show (IFix $ ProgramF [] [IFix $ DefF "foo" [] $ IFix $ ESimpleF $ IFix $ SReturnF $ VSimple $ SVVar "x"])+            `shouldBe`+            "IFix (ProgramF [] [IFix (DefF \"foo\" [] (IFix (ESimpleF (IFix (SReturnF (VSimple (SVVar \"x\")))))))])"++type Name = String++data External = External+    { externalName      :: Name+    , externalEffectful :: Bool+    -- other fields elided+    }+    deriving (Show, Read, Eq, Ord)++data Lit = LInt Int+    | LBool Bool+    deriving (Show, Read, Eq, Ord)++data Val = VTag Name [SimpleVal]+    | VSimple SimpleVal+    deriving (Show, Read, Eq, Ord)++data SimpleVal = SVLit Lit+    | SVVar Name+    deriving (Show, Read, Eq, Ord)++data LPat = LPTag Name [Name]+    | LPUnit+    deriving (Show, Read, Eq, Ord)++data CPat = CPTag Name [Name]+    | CPLit Lit+    | CPDefault+    deriving (Show, Read, Eq, Ord)++{- Original GRIN datatype++data 'Exp+  = Program     [External] [Def]+  | Def         Name [Name] 'Exp+  -- 'Exp+  | EBind       SimpleExp LPat 'Exp+  | ECase       Val [Alt]+  -- Simple 'Exp+  | SApp        Name [SimpleVal]+  | SReturn     Val+  | SStore      Val+  | SFetch      Name+  | SUpdate     Name Val+  | SBlock      'Exp+  -- Alt+  | Alt CPat 'Exp++type SimpleExp = 'Exp+type Alt = 'Exp+type Def = 'Exp+type Program = 'Exp++-}++{- What it really should be++data Program = Program [External] [Def]++data Def = Def Name [Name] 'Exp++data 'Exp+    = EBind SimpleExp LPat 'Exp+    | ECase Val [Alt]+    | ESimple SimpleExp++data SimpleExp+    = SApp Name [SimpleVal]+    | SReturn Val+    | SStore Val+    | SFetch Name+    | SUpdate Name Val+    -- | SBlock 'Exp++data Alt = Alt CPat 'Exp++-}++-- recursion-schemes-ix version++data AST (f :: ASTIdx -> *) (ix :: ASTIdx) where+    -- Program+    ProgramF :: [External] -> [f 'Def] -> AST f 'Program+    -- Def+    DefF :: Name -> [Name] -> f 'Exp -> AST f 'Def+    -- Exp+    EBindF :: f 'SimpleExp -> LPat -> f 'Exp -> AST f 'Exp+    ECaseF :: Val -> [f 'Alt] -> AST f 'Exp+    ESimpleF :: f 'SimpleExp -> AST f 'Exp+    -- SimpleExp+    SAppF :: Name -> [SimpleVal] -> AST f 'SimpleExp+    SReturnF :: Val -> AST f 'SimpleExp+    SStoreF :: Val -> AST f 'SimpleExp+    SFetchF :: Name -> AST f 'SimpleExp+    SUpdateF :: Name -> Val -> AST f 'SimpleExp+    -- Alt+    AltF :: CPat -> f 'Exp -> AST f 'Alt++type Program   = IFix AST 'Program+type Def       = IFix AST 'Def+type Exp       = IFix AST 'Exp+type SimpleExp = IFix AST 'SimpleExp+type Alt       = IFix AST 'Alt++instance IFunctor AST where+    imap = imapDefault++instance ITraversable AST where+    itraverse :: forall ix a b m. (Applicative m, SingI ix)+              => (forall ix. SingI ix => a ix -> m (b ix))+              -> AST a ix+              -> m (AST b ix)+    itraverse f =+      case sing :: Sing ix of+        SProgram -> \case+          ProgramF externs defs -> ProgramF externs <$> traverse (f @'Def) defs+        SDef -> \case+          DefF fn args body -> DefF fn args <$> f @'Exp body+        SExp -> \case+          EBindF e1 pat e2 -> EBindF <$> f @'SimpleExp e1 <*> pure pat <*> f @'Exp e2+          ECaseF x alts -> ECaseF x <$> (traverse (f @'Alt) alts)+          ESimpleF e -> ESimpleF <$> f @'SimpleExp e+        SSimpleExp -> \case+          SAppF fn args -> pure $ SAppF fn args+          SReturnF x -> pure $ SReturnF x+          SStoreF x -> pure $ SStoreF x+          SFetchF l -> pure $ SFetchF l+          SUpdateF l x -> pure $ SUpdateF l x+        SAlt -> \case+          AltF cpat e -> AltF cpat <$> f @'Exp e++instance IShow AST where+    ishowsPrec :: forall ix a. SingI ix+               => (forall ix. SingI ix => Int -> a ix -> ShowS)+               -> Int+               -> AST a ix+               -> ShowS+    ishowsPrec sp p =+      case sing :: Sing ix of+        SProgram -> \case+          ProgramF externs defs -> showParen (p > 10) $+            showString "ProgramF " . showsPrec 11 externs . showString " " . showListWith (sp 0) defs+        SDef -> \case+          DefF fn args body -> showParen (p > 10) $+            showString "DefF " . showsPrec 11 fn . showString " " . showsPrec 11 args . showString " " . sp 11 body+        SExp -> \case+          EBindF e1 pat e2 -> showParen (p > 10) $+            showString "EBindF " . sp 11 e1 . showString " " . showsPrec 11 pat . showString " " . sp 11 e2+          ECaseF x alts -> showParen (p > 10) $+            showString "ECaseF " . showsPrec 11 x . showString " " . showListWith (sp 0) alts+          ESimpleF e -> showParen (p > 10) $+            showString "ESimpleF " . sp 11 e+        SSimpleExp -> \case+          SAppF fn args -> showParen (p > 10) $+            showString "SAppF " . showsPrec 11 fn . showString " " . showsPrec 11 args+          SReturnF x -> showParen (p > 10) $+            showString "SReturnF " . showsPrec 11 x+          SStoreF x -> showParen (p > 10) $+            showString "SStoreF " . showsPrec 11 x+          SFetchF x -> showParen (p > 10) $+            showString "SFetchF " . showsPrec 11 x+          SUpdateF x y -> showParen (p > 10) $+            showString "SUpdateF " . showsPrec 11 x . showString " " . showsPrec 11 y+        SAlt -> \case+          AltF cpat e -> showParen (p > 10) $+            showString "AltF " . showsPrec 11 cpat . showString " " . sp 11 e++data FunNames (ix :: ASTIdx) where+    FNProgram :: { getFunNamesProgram :: Set Name } -> FunNames 'Program+    FNDef :: { getFunNamesDef :: Name } -> FunNames 'Def+    FNOther :: FunNames ix++funnames :: Program -> Set Name+funnames = getFunNamesProgram . cata alg+    where+        alg :: forall ix. SingI ix+            => AST FunNames ix+            -> FunNames ix+        alg =+          case sing :: Sing ix of+            SProgram -> \case+              ProgramF _ defs -> FNProgram $ Set.fromList $ getFunNamesDef <$> defs+            SDef -> \case+              DefF f _ _ -> FNDef f+            _ -> \case+                _ -> FNOther++-- type SSAM = State (Set Name, Int)++-- ssa :: IFix AST 'Exp -> IFix AST 'Exp+-- ssa e = flip evalState (mempty, 1) $+       -- getConst (cata folder e)+    -- >> anaM unfolder (Const (mempty, e))+    -- where+        -- folder :: AST (Const (SSAM ())) ~~> Const (SSAM ())+        -- folder = undefined+        -- unfolder :: forall ix. SingI ix+                 -- => Const (Map Name Int, IFix AST 'Exp) ix+                 -- -> SSAM (AST (Const (Map Name Int, IFix AST 'Exp)) ix)+        -- unfolder = undefined+
+ test/Spec.hs view
@@ -0,0 +1,15 @@+module Main (main) where++import Test.Hspec+import Test.QuickCheck+import qualified FibSpec+import qualified GRINSpec++main :: IO ()+main = hspec spec++spec :: Spec+spec = do+    describe "FibSpec"  FibSpec.spec+    describe "GRINSpec" GRINSpec.spec+