Skip to content

Commit

Permalink
Fixed build for older GHCs. In the process had to remove 'maybeEq', s…
Browse files Browse the repository at this point in the history
…o bumping version to 0.2.
  • Loading branch information
mokus0 committed Jul 13, 2011
1 parent 90efa94 commit 60299eb
Show file tree
Hide file tree
Showing 3 changed files with 13 additions and 36 deletions.
4 changes: 3 additions & 1 deletion dependent-sum.cabal
@@ -1,5 +1,5 @@
name: dependent-sum
version: 0.1
version: 0.2
stability: provisional

cabal-version: >= 1.6
Expand All @@ -15,6 +15,8 @@ synopsis: Dependent sum type
description: Dependent sums and supporting typeclasses for
comparing and formatting them.

tested-with: GHC == 7.0.4, GHC == 6.12.3, GHC == 6.10.4

extra-source-files: examples/*.hs

source-repository head
Expand Down
10 changes: 0 additions & 10 deletions examples/FooGADT.hs
Expand Up @@ -15,21 +15,11 @@ 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 = (==)
Expand Down
35 changes: 10 additions & 25 deletions src/Data/GADT/Compare.hs
@@ -1,13 +1,16 @@
{-# LANGUAGE GADTs, TypeOperators, RankNTypes, TypeFamilies, FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# OPTIONS_GHC -fno-warn-deprecated-flags #-}
{-# LANGUAGE ImpredicativeTypes #-}
module Data.GADT.Compare where

import Data.Maybe
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

Expand All @@ -30,15 +33,14 @@ instance Read (a := a) where
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)
greadsPrec p s = readsPrec p s >>= f
where
f :: (x := x, String) -> [(forall b. (forall a. x := a -> b) -> b, String)]
f (Refl, rest) = 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.
--
Expand All @@ -56,33 +58,16 @@ class GEq f where
--
-- (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
defaultEq x y = isJust (geq x y)

-- |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
defaultNeq x y = isNothing (geq x y)

instance GEq ((:=) a) where
geq Refl Refl = Just Refl
Expand Down

0 comments on commit 60299eb

Please sign in to comment.