ghc-8.10 branch, try to promote SubstScoped

sweirich · Jun 22, 2020 · b5bb206 · b5bb206
1 parent e9ef4d4
commit b5bb206
Show file tree

Hide file tree

Showing 4 changed files with 76 additions and 69 deletions.
diff --git a/debruijn/debruijn.cabal b/debruijn/debruijn.cabal
@@ -39,6 +39,7 @@ library
   build-depends:       base >=4.13,
                        singletons >= 2.6,
                        QuickCheck >= 2.12,
+                       transformers >= 0.5,
                        Cabal
 
   hs-source-dirs:      src
@@ -64,6 +65,7 @@ library
                        RankNTypes
                        ScopedTypeVariables
                        StandaloneDeriving
+                       StandaloneKindSignatures
                        TypeApplications
                        TypeFamilyDependencies
                        TypeFamilies

diff --git a/debruijn/src/Nat.hs b/debruijn/src/Nat.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns -Wno-redundant-constraints #-}
 -- | A simple module of natural numbers (with associated singletons)
-module Nat (
+module Nat {- (
   -- * Nat type, its singleton, and symbols
   Nat(..),SNat(..),SSym0,ZSym0,Sing(..),
 
@@ -20,11 +20,13 @@ module Nat (
   indx, Indx, sIndx, IndxSym0,
 
 
-) where
+) -} where
 
 import Prelude hiding ((!!), take, drop, length)
 import Imports hiding (length, Length, sLength, LengthSym0)
 import Test.QuickCheck((==>),Property,Arbitrary(..),oneof)
+import Data.Singletons.TH.Options
+import Control.Monad.Trans.Class(lift)
 
 $(singletons [d|
     data Nat = Z | S Nat deriving (Eq,Ord)
@@ -88,4 +90,4 @@ instance Show Nat where
 instance Arbitrary Nat where
   arbitrary = oneof [ return Z, S <$> arbitrary ]
   shrink Z     = []
-  shrink (S n) = [n]
+  shrink (S n) = [n]
diff --git a/debruijn/src/SubstScoped.hs b/debruijn/src/SubstScoped.hs
@@ -1,79 +1,83 @@
 -- | Indexing the substitution by a scope, i.e. binding depth
+{-# LANGUAGE TemplateHaskell #-}
 module SubstScoped where
 
 import Imports
-import Nat 
+import Nat
+
+import Control.Monad.Trans.Class
+import Data.Singletons.TH
+import Data.Singletons.TH.Options
+
 
 -- In this file, we will call Nats "Scopes". I.e. they 
 -- are used to describe the number of free variables allowed in 
 -- a term.    
 
+$(withOptions defaultOptions{genSingKindInsts = False} $
+  singletons $ lift [d|
+
+     data Idx :: Nat -> Type where
+         FZ :: Idx (S n)
+         FS :: Idx n -> Idx (S n)
+
+     instance Eq (Idx n) where
+         FZ == FZ = True
+         (FS n) == (FS m) = n == m
+         _ == _ = False
+
+     -- A substitution 
+     -- The parameter 'a' is scope-indexed (i.e. the type 
+     -- describes the number of free variables allowed to 
+     -- appear in the term.)
+     -- Substitution takes terms from scope n to scope m 
+     data Sub (a :: Nat -> Type) (n :: Nat) (m :: Nat) where
+         Inc   :: Sing m -> Sub a n (Plus m n)          
+         (:<)  :: a m -> Sub a n m -> Sub a (S n) m     
+         (:<>) :: Sub a m n -> Sub a n p -> Sub a m p   
+
+     infixr :<     -- like usual cons operator (:)
+     infixr :<>    -- like usual composition  (.)
+
+     --  Identity substitution, leaves all variables alone
+     nilSub :: Sub a n n 
+     nilSub = Inc SZ
+
+     -- Increment, shifts all variables by one
+     incSub :: Sub a n (S n)
+     incSub = Inc (SS SZ)
+
+     -- Singleton, replace 0 with t, leave everything else alone
+     singleSub :: a n -> Sub a (S n) n
+     singleSub t = t :< nilSub
+
+     -- General class for terms that support substitution
+     -- The var construction must bound the index by the scope for the term
+     -- The subst operation changes the scope of an expression
+     class SubstDB (a :: Nat -> Type) where
+        var   :: Idx n -> a n
+        subst :: Sub a n m -> a n -> a m
+
+     add :: Sing m -> Idx n -> Idx (Plus m n)
+     add SZ x = x
+     add (SS m) x = FS (add m x)
+
+     -- Value of the index x in the substitution s
+     applySub :: SubstDB a => Sub a n m -> Idx n -> a m
+     applySub (Inc m)        x  = var (add m x)
+     applySub (ty :< s)     FZ  = ty
+     applySub (ty :< s)  (FS x) = applySub s x
+     applySub (s1 :<> s2)    x  = subst s2 (applySub s1 x)
+
+     -- Used in a substitution when going under a binder
+     lift :: SubstDB a => Sub a n m -> Sub a (S n) (S m)
+     lift s = var FZ :< (s :<> incSub)
+  |])
 
--- | An "indexed" index: (still isomorphic to a natural number)
--- The index is valid in a certain "scope" i.e. must be bounded.
--- (This type is often called Fin.)
-data Idx :: Nat -> Type where
-    FZ :: Idx (S n)
-    FS :: Idx n -> Idx (S n)
-
-instance Eq (Idx n) where
-    FZ == FZ = True
-    (FS n) == (FS m) = n == m
-    _ == _ = False
 
 instance Show (Idx n) where
-    show FZ = "FZ"
-    show (FS n) = "(FS " ++ show n ++ ")"
-
--- | A substitution 
--- The parameter 'a' is scope-indexed (i.e. the type 
--- describes the number of free variables allowed to 
--- appear in the term.)
--- Substitution takes terms from scope n to scope m 
-data Sub (a :: Nat -> Type) (n :: Nat) (m :: Nat) where
-    Inc   :: Sing m -> Sub a n (Plus m n)           --  increment by 1 (shift)                
-    (:<)  :: a m -> Sub a n m -> Sub a (S n) m      --  extend a substitution (like cons)
-    (:<>) :: Sub a m n -> Sub a n p -> Sub a m p    --  compose substitutions
-
-infixr :<     -- like usual cons operator (:)
-infixr :<>    -- like usual composition  (.)
-
--- | Identity substitution, leaves all variables alone
-nilSub :: Sub a n n 
-nilSub = Inc SZ
-
--- | Increment, shifts all variables by one
-incSub :: Sub a n (S n)
-incSub = Inc (SS SZ)
-
--- | Singleton, replace 0 with t, leave everything else alone
-singleSub :: a n -> Sub a (S n) n
-singleSub t = t :< nilSub
-
--- | General class for terms that support substitution
--- The var construction must bound the index by the scope for the term
--- The subst operation changes the scope of an expression
-class SubstDB (a :: Nat -> Type) where
-   var   :: Idx n -> a n
-   subst :: Sub a n m -> a n -> a m
-
-add :: Sing m -> Idx n -> Idx (Plus m n)
-add SZ x = x
-add (SS m) x = FS (add m x)
-
--- | Value of the index x in the substitution s
-applySub :: SubstDB a => Sub a n m -> Idx n -> a m
-applySub (Inc m)        x  = var (add m x)
-applySub (ty :< s)     FZ  = ty
-applySub (ty :< s)  (FS x) = applySub s x
-applySub (s1 :<> s2)    x  = subst s2 (applySub s1 x)
-
--- | Used in a substitution when going under a binder
-lift :: SubstDB a => Sub a n m -> Sub a (S n) (S m)
-lift s = var FZ :< (s :<> incSub)
-
-
-
+   show FZ = "FZ"
+   show (FS n) = "(FS " ++ show n ++ ")"
 
 
 

diff --git a/debruijn/src/SubstTyped.hs b/debruijn/src/SubstTyped.hs
@@ -12,8 +12,7 @@ data Idx (g :: [k]) (t::k) :: Type where
 
 -- | "Environment" heterogenous list
 -- indexed by a list 
-
-data HList (g :: [k]) where
+data HList :: forall k. [k] -> Type where
   HNil  :: HList '[]
   HCons :: t -> HList g -> HList (t:g)