From 27245e24d588a63620ffb7f0276345ac36f8a6ba Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 12 Jul 2019 07:09:45 -0400 Subject: [PATCH] Some API additions and reorganization for Data.Singletons.Sigma (#400) * `SSigma`, the singleton type for `Sigma`, has been added. This fixes #366. * A `Show` instance has been added for `Sigma` (and `SSigma`) by using copious amounts of quantified constraints. The behavior of these instances closely resembles the `Show` implementation for `DPair` in Idris' standard library: https://github.com/idris-lang/Idris-dev/blob/dbe521ff74189df85121abe454f86894de7fd75c/libs/prelude/Prelude/Show.idr#L195-L196 * New functions `fstSigma` and `sndSigma` (as well as their type-level counterparts) have been added. To avoid being a duplicate of `fstSigma`, `projSigma1` has been redefined to have a new type signature that uses continuation-passing style, much like its cousin `projSigma2`. * New functions `currySigma` and `uncurrySigma` have been added. This fixes #359 and supersedes #360. --- CHANGES.md | 30 +++++-- src/Data/Singletons/ShowSing.hs | 11 ++- src/Data/Singletons/Sigma.hs | 135 +++++++++++++++++++++++++++++--- 3 files changed, 154 insertions(+), 22 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index d3135a40..e31561b1 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -121,15 +121,31 @@ Changelog for singletons project As a result, `singletons` no longer generates instances for `SingI` instances for applications of `TyCon{N}` to particular type constructors, as they have been superseded by the instances above. -* Redefine `Σ` such that it is now a partial application of `Sigma`, like so: +* Changes to `Data.Singletons.Sigma`: + * `SSigma`, the singleton type for `Sigma`, is now defined. + * New functions `fstSigma`, `sndSigma`, `FstSigma`, `SndSigma`, `currySigma`, + and `uncurrySigma` have been added. A `Show` instance for `Sigma` has also + been added. + * `projSigma1` has been redefined to use continuation-passing style to more + closely resemble its cousin `projSigma2`. The new type signature of + `projSigma1` is: + + ```hs + projSigma1 :: (forall (fst :: s). Sing fst -> r) -> Sigma s t -> r + ``` - ```haskell - type Σ = Sigma - ``` + The old type signature of `projSigma1` can be found in the `fstSigma` + function. + * `Σ` has been redefined such that it is now a partial application of + `Sigma`, like so: + + ```haskell + type Σ = Sigma + ``` - One benefit of this change is that one no longer needs defunctionalization - symbols in order to partially apply `Σ`. As a result, `ΣSym0`, `ΣSym1`, - and `ΣSym2` have been removed. + One benefit of this change is that one no longer needs defunctionalization + symbols in order to partially apply `Σ`. As a result, `ΣSym0`, `ΣSym1`, + and `ΣSym2` have been removed. * In line with corresponding changes in `base-4.13`, the `Fail`/`sFail` methods of `{P,S}Monad` have been removed in favor of new `{P,S}MonadFail` classes introduced in the `Data.Singletons.Prelude.Monad.Fail` module. These classes diff --git a/src/Data/Singletons/ShowSing.hs b/src/Data/Singletons/ShowSing.hs index bd6f6401..ae0eecc0 100644 --- a/src/Data/Singletons/ShowSing.hs +++ b/src/Data/Singletons/ShowSing.hs @@ -268,12 +268,17 @@ ultimately went with. -} ------------------------------------------------------------ --- WrappedSing instance +-- (S)WrappedSing instances ------------------------------------------------------------ instance ShowSing k => Show (WrappedSing (a :: k)) where - showsPrec p (WrapSing s) = - showParen (p > 10) $ showString "WrapSing " . showsPrec 11 s + showsPrec p (WrapSing s) = showParen (p >= 11) $ + showString "WrapSing {unwrapSing = " . showsPrec 0 s . showChar '}' + :: ShowSing' a => ShowS + +instance ShowSing k => Show (SWrappedSing (ws :: WrappedSing (a :: k))) where + showsPrec p (SWrapSing s) = showParen (p >= 11) $ + showString "SWrapSing {sUnwrapSing = " . showsPrec 0 s . showChar '}' :: ShowSing' a => ShowS ------------------------------------------------------------ diff --git a/src/Data/Singletons/Sigma.hs b/src/Data/Singletons/Sigma.hs index 5fc19be5..a600e027 100644 --- a/src/Data/Singletons/Sigma.hs +++ b/src/Data/Singletons/Sigma.hs @@ -1,12 +1,18 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ImpredicativeTypes #-} -- See Note [Impredicative Σ?] +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- -- | @@ -22,18 +28,34 @@ ---------------------------------------------------------------------------- module Data.Singletons.Sigma - ( Sigma(..), Σ + ( -- * The 'Sigma' type + Sigma(..), Σ + , Sing, SSigma(..), SΣ + + -- * Operations over 'Sigma' + , fstSigma, FstSigma, sndSigma, SndSigma , projSigma1, projSigma2 , mapSigma, zipSigma + , currySigma, uncurrySigma + + -- * Internal utilities + -- $internalutilities + , ShowApply, ShowSingApply + , ShowApply', ShowSingApply' ) where import Data.Kind (Type) import Data.Singletons.Internal +import Data.Singletons.ShowSing -- | A dependent pair. data Sigma (s :: Type) :: (s ~> Type) -> Type where (:&:) :: forall s t fst. Sing (fst :: s) -> t @@ fst -> Sigma s t infixr 4 :&: +instance (ShowSing s, ShowApply t) => Show (Sigma s t) where + showsPrec p ((a :: Sing (fst :: s)) :&: b) = showParen (p >= 5) $ + showsPrec 5 a . showString " :&: " . showsPrec 5 b + :: (ShowSing' fst, ShowApply' t fst) => ShowS -- | Unicode shorthand for 'Sigma'. type Σ = Sigma @@ -48,20 +70,54 @@ case, and the only reason that GHC currently requires this is due to Trac ImpredicativeTypes. -} +-- | The singleton type for 'Sigma'. +data SSigma :: forall s (t :: s ~> Type). Sigma s t -> Type where + (:%&:) :: forall s t (fst :: s) (sfst :: Sing fst) (snd :: t @@ fst). + Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst ':&: snd :: Sigma s t) +infixr 4 :%&: + +type instance Sing = SSigma +instance forall s (t :: s ~> Type) (sig :: Sigma s t). + (ShowSing s, ShowSingApply t) + => Show (SSigma sig) where + showsPrec p ((sa :: Sing ('WrapSing (sfst :: Sing fst))) :%&: (sb :: Sing snd)) = + showParen (p >= 5) $ + showsPrec 5 sa . showString " :&: " . showsPrec 5 sb + :: (ShowSing' fst, ShowSingApply' t fst snd) => ShowS + +instance forall s t (fst :: s) (a :: Sing fst) (b :: t @@ fst). + (SingI fst, SingI b) + => SingI (a ':&: b :: Sigma s t) where + sing = sing :%&: sing + +-- | Unicode shorthand for 'SSigma'. +type SΣ = SSigma + +-- | Project the first element out of a dependent pair. +fstSigma :: forall s t. SingKind s => Sigma s t -> Demote s +fstSigma (a :&: _) = fromSing a + -- | Project the first element out of a dependent pair. -projSigma1 :: forall s t. SingKind s => Sigma s t -> Demote s -projSigma1 (a :&: _) = fromSing a +type family FstSigma (sig :: Sigma s t) :: s where + FstSigma ((_ :: Sing fst) ':&: _) = fst -- | Project the second element out of a dependent pair. --- --- In an ideal setting, the type of 'projSigma2' would be closer to: --- --- @ --- 'projSigma2' :: 'Sing' (sig :: 'Sigma' s t) -> t @@ ProjSigma1 sig --- @ --- --- But promoting 'projSigma1' to a type family is not a simple task. Instead, --- we do the next-best thing, which is to use Church-style elimination. +sndSigma :: forall s t (sig :: Sigma s t). + SingKind (t @@ FstSigma sig) + => SSigma sig -> Demote (t @@ FstSigma sig) +sndSigma (_ :%&: b) = fromSing b + +-- | Project the second element out of a dependent pair. +type family SndSigma (sig :: Sigma s t) :: t @@ FstSigma sig where + SndSigma (_ ':&: b) = b + +-- | Project the first element out of a dependent pair using +-- continuation-passing style. +projSigma1 :: (forall (fst :: s). Sing fst -> r) -> Sigma s t -> r +projSigma1 f (a :&: _) = f a + +-- | Project the second element out of a dependent pair using +-- continuation-passing style. projSigma2 :: forall s t r. (forall (fst :: s). t @@ fst -> r) -> Sigma s t -> r projSigma2 f ((_ :: Sing (fst :: s)) :&: b) = f @fst b @@ -76,3 +132,58 @@ zipSigma :: Sing (f :: a ~> b ~> c) -> Sigma a p -> Sigma b q -> Sigma c r zipSigma f g ((a :: Sing (fstA :: a)) :&: p) ((b :: Sing (fstB :: b)) :&: q) = (f @@ a @@ b) :&: (g @fstA @fstB p q) + +-- | Convert an uncurried function on 'Sigma' to a curried one. +-- +-- Together, 'currySigma' and 'uncurrySigma' witness an isomorphism such that +-- the following identities hold: +-- +-- @ +-- id1 :: forall a (b :: a ~> Type) (c :: 'Sigma' a b ~> Type). +-- (forall (p :: Sigma a b). 'SSigma' p -> c @@ p) +-- -> (forall (p :: Sigma a b). 'SSigma' p -> c @@ p) +-- id1 f = 'uncurrySigma' @a @b @c ('currySigma' @a @b @c f) +-- +-- id2 :: forall a (b :: a ~> Type) (c :: 'Sigma' a b ~> Type). +-- (forall (x :: a) (sx :: Sing x) (y :: b @@ x). Sing ('WrapSing' sx) -> Sing y -> c @@ (sx :&: y)) +-- -> (forall (x :: a) (sx :: Sing x) (y :: b @@ x). Sing ('WrapSing' sx) -> Sing y -> c @@ (sx :&: y)) +-- id2 f = 'currySigma' @a @b @c ('uncurrySigma' @a @b @c f) +-- @ +currySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type). + (forall (p :: Sigma a b). SSigma p -> c @@ p) + -> (forall (x :: a) (sx :: Sing x) (y :: b @@ x). + Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y)) +currySigma f x y = f (x :%&: y) + +-- | Convert a curried function on 'Sigma' to an uncurried one. +-- +-- Together, 'currySigma' and 'uncurrySigma' witness an isomorphism. +-- (Refer to the documentation for 'currySigma' for more details.) +uncurrySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type). + (forall (x :: a) (sx :: Sing x) (y :: b @@ x). + Sing ('WrapSing sx) -> Sing y -> c @@ (sx ':&: y)) + -> (forall (p :: Sigma a b). SSigma p -> c @@ p) +uncurrySigma f (x :%&: y) = f x y + +------------------------------------------------------------ +-- Internal utilities +------------------------------------------------------------ + +{- $internal-utilities + +See the documentation in "Data.Singletons.ShowSing"—in particular, the +Haddocks for 'ShowSing' and `ShowSing'`—for an explanation for why these +classes exist. +-} + +class (forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type) +instance (forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type) + +class Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a) +instance Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a) + +class (forall (x :: a) (z :: Apply f x). ShowSingApply' f x z) => ShowSingApply (f :: a ~> Type) +instance (forall (x :: a) (z :: Apply f x). ShowSingApply' f x z) => ShowSingApply (f :: a ~> Type) + +class Show (Sing z) => ShowSingApply' (f :: a ~> Type) (x :: a) (z :: Apply f x) +instance Show (Sing z) => ShowSingApply' (f :: a ~> Type) (x :: a) (z :: Apply f x)