From b5bb206a20b733cb6b369c218094b8cd71bb4e25 Mon Sep 17 00:00:00 2001 From: Stephanie Weirich Date: Mon, 22 Jun 2020 13:55:48 -0400 Subject: [PATCH] ghc-8.10 branch, try to promote SubstScoped --- debruijn/debruijn.cabal | 2 + debruijn/src/Nat.hs | 8 ++- debruijn/src/SubstScoped.hs | 132 +++++++++++++++++++----------------- debruijn/src/SubstTyped.hs | 3 +- 4 files changed, 76 insertions(+), 69 deletions(-) diff --git a/debruijn/debruijn.cabal b/debruijn/debruijn.cabal index ba919bc..4fde2b2 100644 --- 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 index 78ce474..13f2f82 100644 --- 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] \ No newline at end of file + shrink (S n) = [n] diff --git a/debruijn/src/SubstScoped.hs b/debruijn/src/SubstScoped.hs index 182c96a..aae6be4 100644 --- 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 index 0ca1b22..494dd95 100644 --- 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)