dependent-sum 0.3.2.2 → 0.4
raw patch · 6 files changed
+53/−55 lines, 6 filesdep ~base
Dependency ranges changed: base
Files
- dependent-sum.cabal +1/−1
- examples/FooGADT.hs +4/−4
- src/Data/Dependent/Sum.hs +35/−37
- src/Data/GADT/Compare.hs +5/−8
- src/Data/GADT/Show.hs +7/−3
- src/Data/Some.hs +1/−2
dependent-sum.cabal view
@@ -1,5 +1,5 @@ name: dependent-sum-version: 0.3.2.2+version: 0.4 stability: provisional cabal-version: >= 1.6
examples/FooGADT.hs view
@@ -71,10 +71,10 @@ instance GRead Foo where greadsPrec _ str = case tag of- "Foo" -> [(\k -> k Foo, rest)]- "Bar" -> [(\k -> k Bar, rest)]- "Baz" -> [(\k -> k Baz, rest)]- "Qux" -> [(\k -> k Qux, rest)]+ "Foo" -> [(GReadResult (\k -> k Foo), rest)]+ "Bar" -> [(GReadResult (\k -> k Bar), rest)]+ "Baz" -> [(GReadResult (\k -> k Baz), rest)]+ "Qux" -> [(GReadResult (\k -> k Qux), rest)] _ -> [] where (tag, rest) = splitAt 3 str
src/Data/Dependent/Sum.hs view
@@ -1,12 +1,10 @@ {-# LANGUAGE ExistentialQuantification, GADTs #-} {-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE CPP #-} #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE Safe #-}@@ -36,26 +34,26 @@ -- > AString :: Tag String -- > AnInt :: Tag Int -- --- Then, we have the following valid expressions of type @DSum Tag@:+-- Then, we have the following valid expressions of type @Applicative f => DSum Tag f@: ----- > AString :=> "hello!"--- > AnInt :=> 42+-- > AString ==> "hello!"+-- > AnInt ==> 42 -- --- And we can write functions that consume @DSum Tag@ values by matching, +-- And we can write functions that consume @DSum Tag f@ values by matching, -- such as: -- --- > toString :: DSum Tag -> String--- > toString (AString :=> str) = str--- > toString (AnInt :=> int) = show int+-- > toString :: DSum Tag Identity -> String+-- > toString (AString :=> Identity str) = str+-- > toString (AnInt :=> Identity int) = show int -- --- By analogy to the (key => value) construction for dictionary entries in --- many dynamic languages, we use (key :=> value) as the constructor for --- dependent sums. The :=> operator has very low precedence and binds to --- the right, so if the @Tag@ GADT is extended with an additional constructor--- @Rec :: Tag (DSum Tag)@, then @Rec :=> AnInt :=> 3 + 4@ is parsed as--- would be expected (@Rec :=> (AnInt :=> (3 + 4))@) and has type @DSum Tag@.--- Its precedence is just above that of '$', so @foo bar $ AString :=> "eep"@--- is equivalent to @foo bar (AString :=> "eep")@.+-- By analogy to the (key => value) construction for dictionary entries in+-- many dynamic languages, we use (key :=> value) as the constructor for+-- dependent sums. The :=> and ==> operators have very low precedence and+-- bind to the right, so if the @Tag@ GADT is extended with an additional+-- constructor @Rec :: Tag (DSum Tag Identity)@, then @Rec ==> AnInt ==> 3 + 4@+-- is parsed as would be expected (@Rec ==> (AnInt ==> (3 + 4))@) and has type+-- @DSum Identity Tag@. Its precedence is just above that of '$', so+-- @foo bar $ AString ==> "eep"@ is equivalent to @foo bar (AString ==> "eep")@. data DSum tag f = forall a. !(tag a) :=> f a #if MIN_VERSION_base(4,7,0) deriving Typeable@@ -65,28 +63,28 @@ (==>) :: Applicative f => tag a -> a -> DSum tag f k ==> v = k :=> pure v --- |In order to make a 'Show' instance for @DSum tag@, @tag@ must be able+-- |In order to make a 'Show' instance for @DSum tag f@, @tag@ must be able -- to show itself as well as any value of the tagged type. 'GShow' together -- with this class provides the interface by which it can do so. ----- @ShowTag tag => t@ is conceptually equivalent to something like this--- imaginary syntax: @(forall a. Inhabited (tag a) => Show a) => t@,+-- @ShowTag tag f => t@ is conceptually equivalent to something like this+-- imaginary syntax: @(forall a. Inhabited (tag a) => Show (f a)) => t@, -- where 'Inhabited' is an imaginary predicate that characterizes --- non-empty types, and 'a' does not occur free in 't'.+-- non-empty types, and 'f' and 'a' do not occur free in 't'. -- -- The @Tag@ example type introduced in the 'DSum' section could be given the--- following instances:+-- following instances, among others: -- -- > instance GShow Tag where -- > gshowsPrec _p AString = showString "AString" -- > gshowsPrec _p AnInt = showString "AnInt"--- > instance ShowTag Tag where+-- > instance ShowTag Tag [] where -- > showTaggedPrec AString = showsPrec -- > showTaggedPrec AnInt = showsPrec -- class GShow tag => ShowTag tag f where -- |Given a value of type @tag a@, return the 'showsPrec' function for - -- the type parameter @a@.+ -- the type @f a@. showTaggedPrec :: tag a -> Int -> f a -> ShowS instance Show (f a) => ShowTag ((:=) a) f where@@ -110,17 +108,17 @@ class GRead tag => ReadTag tag f where readTaggedPrec :: tag a -> Int -> ReadS (f a) --- |In order to make a 'Read' instance for @DSum tag@, @tag@ must be able+-- |In order to make a 'Read' instance for @DSum tag f@, @tag@ must be able -- to parse itself as well as any value of the tagged type. 'GRead' together -- with this class provides the interface by which it can do so. ----- @ReadTag tag => t@ is conceptually equivalent to something like this--- imaginary syntax: @(forall a. Inhabited (tag a) => Read a) => t@,+-- @ReadTag tag f => t@ is conceptually equivalent to something like this+-- imaginary syntax: @(forall a. Inhabited (tag a) => Read (f a)) => t@, -- where 'Inhabited' is an imaginary predicate that characterizes --- non-empty types, and 'a' does not occur free in 't'.+-- non-empty types, and 'f' and 'a' do not occur free in 't'. -- -- The @Tag@ example type introduced in the 'DSum' section could be given the--- following instances:+-- following instances, among others: -- -- > instance GRead Tag where -- > greadsPrec _p str = case tag of@@ -128,7 +126,7 @@ -- > "AnInt" -> [(\k -> k AnInt, rest)] -- > _ -> [] -- > where (tag, rest) = break isSpace str--- > instance ReadTag Tag where+-- > instance ReadTag Tag [] where -- > readTaggedPrec AString = readsPrec -- > readTaggedPrec AnInt = readsPrec -- @@ -148,7 +146,7 @@ instance ReadTag tag f => Read (DSum tag f) where readsPrec p = readParen (p > 1) $ \s -> concat- [ withTag $ \tag ->+ [ getGReadResult withTag $ \tag -> [ (tag :=> val, rest'') | (val, rest'') <- readTaggedPrec tag 1 rest' ]@@ -157,7 +155,7 @@ , con == " :=> " ] --- |In order to test @DSum tag@ for equality, @tag@ must know how to test+-- |In order to test @DSum tag f@ for equality, @tag@ must know how to test -- both itself and its tagged values for equality. 'EqTag' defines -- the interface by which they are expected to do so. -- @@ -167,7 +165,7 @@ -- > geq AString AString = Just Refl -- > geq AnInt AnInt = Just Refl -- > geq _ _ = Nothing--- > instance EqTag Tag where+-- > instance EqTag Tag [] where -- > eqTagged AString AString = (==) -- > eqTagged AnInt AnInt = (==) -- @@ -175,7 +173,7 @@ -- compared, so it only needs to consider the cases where 'gcompare' returns 'GEQ'. class GEq tag => EqTag tag f where -- |Given two values of type @tag a@ (for which 'gcompare' returns 'GEQ'),- -- return the '==' function for the type @a@.+ -- return the '==' function for the type @f a@. eqTagged :: tag a -> tag a -> f a -> f a -> Bool instance Eq (f a) => EqTag ((:=) a) f where@@ -186,7 +184,7 @@ Refl <- geq t1 t2 return (eqTagged t1 t2 x1 x2) --- |In order to compare @DSum tag@ values, @tag@ must know how to compare+-- |In order to compare @DSum tag f@ values, @tag@ must know how to compare -- both itself and its tagged values. 'OrdTag' defines the -- interface by which they are expected to do so. -- @@ -197,7 +195,7 @@ -- > gcompare AString AnInt = GLT -- > gcompare AnInt AString = GGT -- > gcompare AnInt AnInt = GEQ--- > instance OrdTag Tag where+-- > instance OrdTag Tag [] where -- > compareTagged AString AString = compare -- > compareTagged AnInt AnInt = compare -- @@ -205,7 +203,7 @@ -- 'gcompare' returns 'GEQ'. class (EqTag tag f, GCompare tag) => OrdTag tag f where -- |Given two values of type @tag a@ (for which 'gcompare' returns 'GEQ'),- -- return the 'compare' function for the type @a@.+ -- return the 'compare' function for the type @f a@. compareTagged :: tag a -> tag a -> f a -> f a -> Ordering instance Ord (f a) => OrdTag ((:=) a) f where
src/Data/GADT/Compare.hs view
@@ -2,7 +2,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE DeriveDataTypeable #-} {-# OPTIONS_GHC -fno-warn-deprecated-flags #-}-{-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE CPP #-} #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 {-# LANGUAGE PolyKinds #-}@@ -57,8 +56,8 @@ instance GRead ((:=) a) where greadsPrec p s = readsPrec p s >>= f where- f :: forall x. (x := x, String) -> [(forall b. (forall a. x := a -> b) -> b, String)]- f (Refl, rest) = return ((\x -> x Refl) :: forall b. (forall a. x := a -> b) -> b, rest)+ f :: forall x. (x := x, String) -> [(GReadResult ((:=) x), String)]+ f (Refl, rest) = return (GReadResult (\x -> x Refl) , rest) -- |A class for type-contexts which contain enough information -- to (at least in some cases) decide the equality of types @@ -154,9 +153,9 @@ instance GRead (GOrdering a) where greadsPrec _ s = case con of- "GGT" -> [(\x -> x GGT, rest)]- "GEQ" -> [(\x -> x GEQ, rest)]- "GLT" -> [(\x -> x GLT, rest)]+ "GGT" -> [(GReadResult (\x -> x GGT), rest)]+ "GEQ" -> [(GReadResult (\x -> x GEQ), rest)]+ "GLT" -> [(GReadResult (\x -> x GLT), rest)] _ -> [] where (con, rest) = splitAt 3 s @@ -170,5 +169,3 @@ defaultCompare :: GCompare f => f a -> f b -> Ordering defaultCompare x y = weakenOrdering (gcompare x y)--
src/Data/GADT/Show.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE CPP #-} #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE Safe #-}@@ -23,9 +23,12 @@ gshow :: (GShow t) => t a -> String gshow x = gshows x "" +newtype GReadResult t = GReadResult+ { getGReadResult :: forall b . (forall a . t a -> b) -> b }+ -- |@GReadS t@ is equivalent to @ReadS (forall b. (forall a. t a -> b) -> b)@, which is -- in turn equivalent to @ReadS (Exists t)@ (with @data Exists t where Exists :: t a -> Exists t@)-type GReadS t = String -> [(forall b. (forall a. t a -> b) -> b, String)]+type GReadS t = String -> [(GReadResult t, String)] -- |'Read'-like class for 1-type-parameter GADTs. Unlike 'GShow', this one cannot be -- mechanically derived from a 'Read' instance because 'greadsPrec' must choose the phantom@@ -37,7 +40,8 @@ greads = greadsPrec (-1) gread :: GRead t => String -> (forall a. t a -> b) -> b-gread s = hd [f | (f, "") <- greads s]+gread s g = case hd [f | (f, "") <- greads s] of+ GReadResult res -> res g where hd (x:_) = x hd _ = error "gread: no parse"
src/Data/Some.hs view
@@ -1,6 +1,5 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE CPP #-} #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE Safe #-}@@ -28,7 +27,7 @@ instance GRead f => Read (Some f) where readsPrec p = readParen (p>10) $ \s ->- [ (withTag This, rest')+ [ (getGReadResult withTag This, rest') | let (con, rest) = splitAt 5 s , con == "This " , (withTag, rest') <- greadsPrec 11 rest