Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add equivalence with :~: #9

Merged
merged 1 commit into from Nov 15, 2016
Merged

Add equivalence with :~: #9

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
23 changes: 23 additions & 0 deletions src/Data/Eq/Type.hs
View file
Open in desktop
Expand Up @@ -5,6 +5,11 @@
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707
{-# LANGUAGE RoleAnnotations #-}
#endif
#if defined(__GLASGOW_HASKELL__) && MIN_VERSION_base(4,7,0)
#define HAS_DATA_TYPE_EQUALITY 1
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
#endif

-----------------------------------------------------------------------------
-- |
Expand Down Expand Up @@ -40,6 +45,12 @@ module Data.Eq.Type
, lower
, lower2
, lower3
#endif
#ifdef HAS_DATA_TYPE_EQUALITY
-- * ':~:' equivalence
-- | "Data.Type.Equality" GADT definition is equivalent in power
, fromLeibniz
, toLeibniz
#endif
) where

Expand All @@ -48,6 +59,10 @@ import Control.Category
import Data.Semigroupoid
import Data.Groupoid

#ifdef HAS_DATA_TYPE_EQUALITY
import qualified Data.Type.Equality as Eq
#endif

infixl 4 :=

-- | Leibnizian equality states that two things are equal if you can
Expand Down Expand Up @@ -128,3 +143,11 @@ lower3 :: f a c d := f b c d -> a := b
lower3 eq = unlower3 (subst eq (Lower3 refl :: Lower3 (f a c d) (f a c d)))

#endif

#ifdef HAS_DATA_TYPE_EQUALITY
fromLeibniz :: a := b -> a Eq.:~: b
fromLeibniz a = subst a Eq.Refl

toLeibniz :: a Eq.:~: b -> a := b
toLeibniz Eq.Refl = refl
#endif