Repository : ssh://[email protected]/base On branch : master Link : http://ghc.haskell.org/trac/ghc/changeset/3323f41778c5b5209cfd905aec4b7558df7755ee/base
>--------------------------------------------------------------- commit 3323f41778c5b5209cfd905aec4b7558df7755ee Author: Iavor S. Diatchki <[email protected]> Date: Sun Sep 8 14:38:47 2013 -0700 Redo <= with a type synonym instead of a class, add instance for boolean singletons, remove (-) >--------------------------------------------------------------- 3323f41778c5b5209cfd905aec4b7558df7755ee GHC/TypeLits.hs | 35 +++++++++++++++++++++++++++-------- 1 file changed, 27 insertions(+), 8 deletions(-) diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs index c2e4906..f71f654 100644 --- a/GHC/TypeLits.hs +++ b/GHC/TypeLits.hs @@ -8,9 +8,9 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} -- for <= {-# LANGUAGE RankNTypes #-} -- for SingI magic {-# LANGUAGE ScopedTypeVariables #-} -- for SingI magic +{-# LANGUAGE ConstraintKinds #-} -- for <= {-# OPTIONS_GHC -XNoImplicitPrelude #-} {-| This module is an internal GHC module. It declares the constants used in the implementation of type-level natural numbers. The programmer interface @@ -29,10 +29,9 @@ module GHC.TypeLits -- * Functions on type nats , type (<=), type (<=?), type (+), type (*), type (^) - , type (-) -- * Comparing for equality - , type (:~:) (..), eqSingNat, eqSingSym + , type (:~:) (..), eqSingNat, eqSingSym, eqSingBool -- * Destructing type-nat singletons. , isZero, IsZero(..) @@ -83,6 +82,10 @@ newtype instance Sing (n :: Nat) = SNat Integer newtype instance Sing (n :: Symbol) = SSym String +data instance Sing (n :: Bool) where + SFalse :: Sing False + STrue :: Sing True + -------------------------------------------------------------------------------- -- | The class 'SingI' provides a \"smart\" constructor for singleton types. @@ -99,11 +102,13 @@ class SingI a where singByProxy :: SingI n => proxy n -> Sing n singByProxy _ = sing +instance SingI False where sing = SFalse +instance SingI True where sing = STrue + -------------------------------------------------------------------------------- -- | Comparison of type-level naturals. -class (m <=? n) ~ True => (m :: Nat) <= (n :: Nat) -instance ((m <=? n) ~ True) => m <= n +type x <= y = (x <=? y) ~ True type family (m :: Nat) <=? (n :: Nat) :: Bool @@ -116,9 +121,7 @@ type family (m :: Nat) * (n :: Nat) :: Nat -- | Exponentiation of type-level naturals. type family (m :: Nat) ^ (n :: Nat) :: Nat --- | Subtraction of type-level naturals. --- Note that this operation is unspecified for some inputs. -type family (m :: Nat) - (n :: Nat) :: Nat + -------------------------------------------------------------------------------- @@ -144,6 +147,13 @@ instance SingE (KindParam :: KindIs Symbol) where type DemoteRep (KindParam :: KindIs Symbol) = String fromSing (SSym s) = s + +instance SingE (KindParam :: KindIs Bool) where + type DemoteRep (KindParam :: KindIs Bool) = Bool + fromSing SFalse = False + fromSing STrue = True + + {- | A convenient name for the type used to representing the values for a particular singleton family. For example, @Demote 2 ~ Integer@, and also @Demote 3 ~ Integer@, but @Demote "Hello" ~ String@. -} @@ -185,6 +195,9 @@ instance ToSing (KindParam :: KindIs Nat) where instance ToSing (KindParam :: KindIs Symbol) where toSing n = Just (incoherentForgetSing (SSym n)) +instance ToSing (KindParam :: KindIs Bool) where + toSing False = Just (SomeSing SFalse) + toSing True = Just (SomeSing STrue) {- PRIVATE: @@ -329,4 +342,10 @@ eqSingSym x y | otherwise = Nothing +eqSingBool :: Sing (m :: Bool) -> Sing (n :: Bool) -> Maybe (m :~: n) +eqSingBool STrue STrue = Just Refl +eqSingBool SFalse SFalse = Just Refl +eqSingBool _ _ = Nothing + + _______________________________________________ ghc-commits mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-commits
