packages feed

dependent-sum (empty) → 0.1

raw patch · 6 files changed

+504/−0 lines, 6 filesdep +basesetup-changed

Dependencies added: base

Files

+ Setup.lhs view
@@ -0,0 +1,5 @@+#!/usr/bin/env runhaskell++> import Distribution.Simple+> main = defaultMain+
+ dependent-sum.cabal view
@@ -0,0 +1,29 @@+name:                   dependent-sum+version:                0.1+stability:              provisional++cabal-version:          >= 1.6+build-type:             Simple++author:                 James Cook <mokus@deepbondi.net>+maintainer:             James Cook <mokus@deepbondi.net>+license:                PublicDomain+homepage:               https://github.com/mokus0/dependent-sum++category:               Data, Dependent Types+synopsis:               Dependent sum type+description:            Dependent sums and supporting typeclasses for+                        comparing and formatting them.++extra-source-files:     examples/*.hs++source-repository head+  type:     git+  location: git://github.com/mokus0/dependent-sum.git++Library+  hs-source-dirs:       src+  exposed-modules:      Data.Dependent.Sum+                        Data.GADT.Compare+                        Data.GADT.Show+  build-depends:        base >= 3 && <5
+ examples/FooGADT.hs view
@@ -0,0 +1,103 @@+{-# LANGUAGE GADTs #-}+module FooGADT where++import Data.Dependent.Sum+import Data.GADT.Show+import Data.GADT.Compare++data Foo a where+    Foo :: Foo Double+    Bar :: Foo Int+    Baz :: Foo String+    Qux :: Foo Double++instance Eq (Foo a) where+    (==) = defaultEq++instance GEq Foo where+    -- either 'geq' or 'maybeEq' are sufficient, but both+    -- are given here for illustration of how to define them.+    +    geq Foo Foo = Just Refl+    geq Bar Bar = Just Refl+    geq Baz Baz = Just Refl+    geq Qux Qux = Just Refl+    geq _   _   = Nothing+    +    maybeEq Foo Foo y n = y+    maybeEq Bar Bar y n = y+    maybeEq Baz Baz y n = y+    maybeEq Qux Qux y n = y+    maybeEq _   _   y n = n+    ++instance EqTag Foo where+    eqTagged Foo Foo = (==)+    eqTagged Bar Bar = (==)+    eqTagged Baz Baz = (==)+    eqTagged Qux Qux = (==)+    eqTagged _   _   = const (const False)++instance GCompare Foo where+    gcompare Foo Foo = GEQ+    gcompare Foo _   = GLT+    gcompare _   Foo = GGT+    +    gcompare Bar Bar = GEQ+    gcompare Bar _   = GLT+    gcompare _   Bar = GGT+    +    gcompare Baz Baz = GEQ+    gcompare Baz _   = GLT+    gcompare _   Baz = GGT+    +    gcompare Qux Qux = GEQ++instance OrdTag Foo where+    compareTagged Foo Foo = compare+    compareTagged Bar Bar = compare+    compareTagged Baz Baz = compare+    compareTagged Qux Qux = compare+    +    compareTagged _   _   = error "OrdTag (Foo): bad case"++instance Show (Foo a) where+    showsPrec _ Foo      = showString "Foo"+    showsPrec _ Bar      = showString "Bar"+    showsPrec _ Baz      = showString "Baz"+    showsPrec _ Qux      = showString "Qux"++instance GShow Foo where+    gshowsPrec = showsPrec++instance ShowTag Foo where+    showTaggedPrec Foo = showsPrec+    showTaggedPrec Bar = showsPrec+    showTaggedPrec Baz = showsPrec+    showTaggedPrec Qux = showsPrec+++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)]+        _     -> []+        where (tag, rest) = splitAt 3 str++instance ReadTag Foo where+    readTaggedPrec Foo = readsPrec+    readTaggedPrec Bar = readsPrec+    readTaggedPrec Baz = readsPrec+    readTaggedPrec Qux = readsPrec+++foo x = Foo :=> x+bar x = Bar :=> x+baz x = Baz :=> x+qux x = Qux :=> x+++xs = [foo pi, bar 100, baz "hello world", qux (exp 1)]+xs' = read (show xs) `asTypeOf` xs
+ src/Data/Dependent/Sum.hs view
@@ -0,0 +1,175 @@+{-# LANGUAGE ExistentialQuantification, GADTs #-}+module Data.Dependent.Sum where++import Data.GADT.Show+import Data.GADT.Compare+import Data.Typeable++import Data.Maybe (fromMaybe)++-- |A basic dependent sum type; the first component is a tag that specifies +-- the type of the second;  for example, think of a GADT such as:+-- +-- > data Tag a where+-- >    AString :: Tag String+-- >    AnInt   :: Tag Int+-- +-- Then, we have the following valid expressions of type @DSum Tag@:+--+-- > AString :=> "hello!"+-- > AnInt   :=> 42+-- +-- And we can write functions that consume @DSum Tag@ values by matching, +-- such as:+-- +-- > toString :: DSum Tag -> String+-- > toString (AString :=> str) = str+-- > toString (AnInt   :=> 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")@.+data DSum tag = forall a. !(tag a) :=> a+infixr 1 :=>++instance Typeable1 t => Typeable (DSum t) where+    typeOf ds = mkTyConApp dSumCon [typeOfT]+        where+            dSumCon = mkTyCon "Data.Dependent.Sum.DSum"+            typeOfT = typeOf1 $ (undefined :: DSum f -> f a) ds++-- |In order to make a 'Show' instance for @DSum tag@, @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.+--+-- @GShow tag => t@ is conceptually equivalent to something like this+-- imaginary syntax:  @(forall a. Inhabited (tag a) => Show a) => t@,+-- where 'Inhabited' is an imaginary predicate that characterizes +-- non-empty types, and 'a' does not occur free in 't'.+--+-- The @Tag@ example type introduced in the 'DSum' section could be given the+-- following instances:+-- +-- > instance GShow Tag where+-- >     gshowsPrec _showsValPrec _p AString = showString "AString"+-- >     gshowsPrec _showsValPrec _p AnInt   = showString "AnInt"+-- > instance ShowTag Tag where+-- >     showTaggedPrec AString = showsPrec+-- >     showTaggedPrec AnInt   = showsPrec+-- +class GShow tag => ShowTag tag where+    -- |Given a value of type @tag a@, return the 'showsPrec' function for +    -- the type parameter @a@.+    showTaggedPrec :: tag a -> Int ->     a -> ShowS++instance Show a => ShowTag ((:=) a) where+    showTaggedPrec Refl = showsPrec++-- This instance is questionable.  It works, but is pretty useless.+instance Show a => ShowTag (GOrdering a) where+    showTaggedPrec GEQ = showsPrec+    showTaggedPrec _   = \p _ -> showParen (p > 10)+        ( showString "error "+        . shows "type information lost into the mists of oblivion"+        )++instance ShowTag tag => Show (DSum tag) where+    showsPrec p (tag :=> value) = showParen (p >= 10)+        ( gshowsPrec 0 tag+        . showString " :=> "+        . showTaggedPrec tag 1 value+        )++class GRead tag => ReadTag tag where+    readTaggedPrec :: tag a -> Int -> ReadS a++instance Read a => ReadTag ((:=) a) where+    readTaggedPrec Refl = readsPrec++-- This instance is questionable.  It works, but is partial (and is also pretty useless)+-- instance Read a => ReadTag (GOrdering a) where+--     readTaggedPrec GEQ = readsPrec+--     readTaggedPrec tag = \p -> readParen (p>10) $ \s ->+--         [ (error msg, rest')+--         | let (con, rest) = splitAt 6 s+--         , con == "error "+--         , (msg, rest') <- reads rest :: [(String, String)]+--         ]++instance ReadTag tag => Read (DSum tag) where+    readsPrec p = readParen (p > 1) $ \s -> +        concat+            [ withTag $ \tag ->+                [ (tag :=> val, rest'')+                | (val, rest'') <- readTaggedPrec tag 1 rest'+                ]+            | (withTag, rest) <- greadsPrec p s+            , let (con, rest') = splitAt 5 rest+            , con == " :=> "+            ]++-- |In order to test @DSum tag@ 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.+-- +-- Continuing the @Tag@ example from the 'DSum' section, we can define:+-- +-- > instance GEq Tag where+-- >     geq AString AString = Just Refl+-- >     geq AString AnInt   = Nothing+-- >     geq AnInt   AString = Nothing+-- >     geq AnInt   AnInt   = Just Refl+-- > instance EqTag Tag where+-- >     eqTagged AString AString = (==)+-- >     eqTagged AnInt   AnInt   = (==)+-- +-- Note that 'eqTagged' is not called until after the tags have been+-- compared, so it only needs to consider the cases where 'gcompare' returns 'GEQ'.+class GEq tag => EqTag tag where+    -- |Given two values of type @tag a@ (for which 'gcompare' returns 'GEQ'),+    -- return the '==' function for the type @a@.+    eqTagged :: tag a -> tag a -> a -> a -> Bool++instance Eq a => EqTag ((:=) a) where+    eqTagged Refl Refl = (==)++instance EqTag tag => Eq (DSum tag) where+    (t1 :=> x1) == (t2 :=> x2)  = fromMaybe False $ do+        Refl <- geq t1 t2+        return (eqTagged t1 t2 x1 x2)++-- |In order to compare @DSum tag@ 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.+-- +-- Continuing the @Tag@ example from the 'EqTag' section, we can define:+-- +-- > instance GCompare Tag where+-- >     gcompare AString AString = GEQ+-- >     gcompare AString AnInt   = GLT+-- >     gcompare AnInt   AString = GGT+-- >     gcompare AnInt   AnInt   = GEQ+-- > instance OrdTag Tag where+-- >     compareTagged AString AString = compare+-- >     compareTagged AnInt   AnInt   = compare+-- +-- As with 'eqTagged', 'compareTagged' only needs to consider cases where+-- 'gcompare' returns 'GEQ'.+class (EqTag tag, GCompare tag) => OrdTag tag where+    -- |Given two values of type @tag a@ (for which 'gcompare' returns 'GEQ'),+    -- return the 'compare' function for the type @a@.+    compareTagged :: tag a -> tag a -> a -> a -> Ordering++instance Ord a => OrdTag ((:=) a) where+    compareTagged Refl Refl = compare++instance OrdTag tag => Ord (DSum tag) where+    compare (t1 :=> x1) (t2 :=> x2)  = case gcompare t1 t2 of+        GLT -> LT+        GGT -> GT+        GEQ -> compareTagged t1 t2 x1 x2
+ src/Data/GADT/Compare.hs view
@@ -0,0 +1,165 @@+{-# LANGUAGE GADTs, TypeOperators, RankNTypes, TypeFamilies, FlexibleInstances #-}+{-# LANGUAGE DeriveDataTypeable #-}+module Data.GADT.Compare where++import Data.GADT.Show+import Data.Typeable++-- |A GADT witnessing equality of two types.  Its only inhabitant is 'Refl'.+data a := b where+    -- |A value witnessing the fact that two types are in fact the same.+    Refl :: a := a+    deriving Typeable++instance Eq (a := b) where+    Refl == Refl = True++instance Ord (a := b) where+    compare Refl Refl = EQ++instance Show (a := b) where+    showsPrec _ Refl = showString "Refl"++instance GShow ((:=) a) where+    gshowsPrec _ Refl = showString "Refl"++instance Read (a := a) where+    readsPrec _ s = case con of+        "Refl"  -> [(Refl, rest)]+        _       -> []+        where (con,rest) = splitAt 4 s++instance GRead ((:=) a) where+    greadsPrec p s = do+        (Refl, rest) <- readsPrec p s :: [(x := x, String)]+        return (\x -> x Refl, rest)++-- |A class for type-contexts which contain enough information+-- to (at least in some cases) decide the equality of types +-- occurring within them.+-- +-- Minimal instance declaration is either 'geq' or 'maybeEq'.+class GEq f where+    -- |Produce a witness of type-equality, if one exists.+    -- +    -- A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:+    -- +    -- > extract :: GEq tag => tag a -> DSum tag -> Maybe a+    -- > extract t1 (t2 :=> x) = do+    -- >     Refl <- geq t1 t2+    -- >     return x+    -- +    -- Or in a list comprehension:+    -- +    -- > extractMany :: GEq tag => tag a -> [DSum tag] -> [a]+    -- > extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)]+    --+    -- (Making use of the 'DSum' type from "Data.Dependent.Sum" in both examples)+    geq :: f a -> f b -> Maybe (a := b)+    geq x y = maybeEq x y (Just Refl) Nothing+    +    -- |An interesting alternative formulation:+    -- This one is nice because it's purely type-level, which means+    -- that in some cases the type checker can statically prove+    -- that the 'f' case is unreachable.  In other cases, it can lead+    -- to nice concise code such as:+    -- +    -- > extract :: GEq tag => tag a -> DSum tag -> Maybe a+    -- > extract t1 (t2 :=> x) = maybeEq t1 t2 (Just x) Nothing+    -- +    -- Sometimes, though, it can be hard to get the 'Refl' case's type to unify+    -- with the assumptions properly.+    maybeEq :: f a -> f b -> ((a ~ b) => c) -> c -> c+    maybeEq x y f z = case geq x y of+        Just Refl   -> f+        Nothing     -> z++-- |If 'f' has a 'GEq' instance, this function makes a suitable default +-- implementation of '(==)'.+defaultEq :: GEq f => f a -> f b -> Bool+defaultEq x y = maybeEq x y True False++-- |If 'f' has a 'GEq' instance, this function makes a suitable default +-- implementation of '(/=)'.+defaultNeq :: GEq f => f a -> f b -> Bool+defaultNeq x y = maybeEq x y False True++instance GEq ((:=) a) where+    geq Refl Refl = Just Refl++-- This instance seems nice, but it's simply not right:+-- +-- > instance GEq StableName where+-- >     geq sn1 sn2+-- >         | sn1 == unsafeCoerce sn2+-- >             = Just (unsafeCoerce Refl)+-- >         | otherwise     = Nothing+-- +-- Proof:+-- +-- > x <- makeStableName id :: IO (StableName (Int -> Int))+-- > y <- makeStableName id :: IO (StableName ((Int -> Int) -> Int -> Int))+-- > +-- > let Just boom = geq x y+-- > let coerce :: (a := b) -> a -> b; coerce Refl = id+-- > +-- > coerce boom (const 0) id 0+-- > let "Illegal Instruction" = "QED."+-- +-- The core of the problem is that 'makeStableName' only knows the closure+-- it is passed to, not any type information.  Together with the fact that+-- the same closure has the same StableName each time 'makeStableName' is +-- called on it, there is serious potential for abuse when a closure can +-- be given many incompatible types.+++-- |A type for the result of comparing GADT constructors; the type parameters+-- of the GADT values being compared are included so that in the case where +-- they are equal their parameter types can be unified.+data GOrdering a b where+    GLT :: GOrdering a b+    GEQ :: GOrdering t t+    GGT :: GOrdering a b+    deriving Typeable++-- |TODO: Think of a better name+--+-- This operation forgets the phantom types of a 'GOrdering' value.+weakenOrdering :: GOrdering a b -> Ordering+weakenOrdering GLT = LT+weakenOrdering GEQ = EQ+weakenOrdering GGT = GT++instance Eq (GOrdering a b) where+    x == y =+        weakenOrdering x == weakenOrdering y++instance Ord (GOrdering a b) where+    compare x y = compare (weakenOrdering x) (weakenOrdering y)++instance Show (GOrdering a b) where+    showsPrec _ GGT = showString "GGT"+    showsPrec _ GEQ = showString "GEQ"+    showsPrec _ GLT = showString "GLT"++instance GShow (GOrdering a) where+    gshowsPrec = showsPrec++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)]+        _       -> []+        where (con, rest) = splitAt 3 s++-- |Type class for orderable GADT-like structures.  When 2 things are equal,+-- must return a witness that their parameter types are equal as well (GEQ).+-- |Type class for comparable GADT-like structures.  When 2 things are equal,+-- must return a witness that their parameter types are equal as well ('GEQ').+class GEq f => GCompare f where+    gcompare :: f a -> f b -> GOrdering a b++instance GCompare ((:=) a) where+    gcompare Refl Refl = GEQ+
+ src/Data/GADT/Show.hs view
@@ -0,0 +1,27 @@+{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}+module Data.GADT.Show where++-- |'Show'-like class for 1-type-parameter GADTs+class GShow t where+    gshowsPrec :: Int -> t a -> ShowS+++gshows :: GShow t => t a -> ShowS+gshows = gshowsPrec (-1)++gshow :: (GShow t) => t a -> String+gshow x = gshows x ""+++type GReadS t = String -> [(forall b. (forall a. t a -> b) -> b, String)]+class GRead t where+    greadsPrec :: Int -> GReadS t++greads :: GRead t => GReadS t+greads = greadsPrec (-1)++gread :: GRead t => String -> (forall a. t a -> b) -> b+gread s = hd [f | (f, "") <- greads s]+    where+        hd (x:_) = x+        hd _ = error "gread: no parse"