eq (empty) → 0.1.0

raw patch · 4 files changed

+166/−0 lines, 4 filesdep +basesetup-changed

Dependencies added: base

Files

• Data/Eq/Type.hs +97/−0
• LICENSE +30/−0
• Setup.lhs +7/−0
• eq.cabal +32/−0

@@ -0,0 +1,97 @@+{-# LANGUAGE Rank2Types, TypeOperators #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Type.Eq+-- Copyright   :  (C) 2011 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  provisional+-- Portability :  rank2 types, type operators, type families (optional)+--+-- Leibnizian equality. Injectivity in the presence of type families +-- is provided by a generalization of a trick by Oleg Kiselyv posted here:+--+-- <http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html>+----------------------------------------------------------------------------++module Data.Eq.Type+  ( (:=)(..)+  , refl+  , trans+  , symm +  , coerce+  , lift+  , lift2, lift2'+  , lift3, lift3'+#ifdef LANGUAGE_TypeFamilies+  , lower+  , lower2+  , lower3+#endif+  ) where++import Prelude ()+import Control.Category ++infixl 4 :=++data a := b = Refl { subst :: forall c. c a -> c b } ++refl :: a := a+refl = Refl id++newtype Coerce a = Coerce { uncoerce :: a } +coerce :: a := b -> a -> b+coerce f = uncoerce . subst f . Coerce++instance Category (:=) where+  id = Refl id+  (.) = subst++trans :: a := b -> b := c -> a := c+trans = (>>>)++newtype Symm p a b = Symm { unsymm :: p b a } +symm :: (a := b) -> (b := a)+symm a = unsymm (subst a (Symm id))++newtype Lift f a b = Lift { unlift :: f a := f b } +lift :: a := b -> f a := f b+lift a = unlift (subst a (Lift id))++newtype Lift2 f c a b = Lift2 { unlift2 :: f a c := f b c }  +lift2 :: a := b -> f a c := f b c+lift2 a = unlift2 (subst a (Lift2 id))++lift2' :: a := b -> c := d -> f a c := f b d+lift2' ab cd = lift2 ab . lift cd++newtype Lift3 f c d a b = Lift3 { unlift3 :: f a c d := f b c d } +lift3 :: a := b -> f a c d := f b c d+lift3 a = unlift3 (subst a (Lift3 id))++lift3' :: a := b -> c := d -> e := f -> g a c e := g b d f+lift3' ab cd ef = lift3 ab . lift2 cd . lift ef++#ifdef LANGUAGE_TypeFamilies++type family Inj f :: *+type instance Inj (f a) = a+newtype Lower a b = Lower { unlower :: Inj a := Inj b }+lower :: f a := f b -> a := b+lower eq = unlower (subst eq (Lower id :: Lower (f a) (f a)))++type family Inj2 f :: *+type instance Inj2 (f a b) = a+newtype Lower2 a b = Lower2 { unlower2 :: Inj2 a := Inj2 b }+lower2 :: f a c := f b c -> a := b+lower2 eq = unlower2 (subst eq (Lower2 id :: Lower2 (f a c) (f a c)))++type family Inj3 f :: *+type instance Inj3 (f a b c) = a+newtype Lower3 a b = Lower3 { unlower3 :: Inj3 a := Inj3 b }+lower3 :: f a c d := f b c d -> a := b+lower3 eq = unlower3 (subst eq (Lower3 id :: Lower3 (f a c d) (f a c d)))++#endif

@@ -0,0 +1,30 @@+Copyright 2010-2011 Edward Kmett++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,7 @@+#!/usr/bin/runhaskell+> module Main (main) where++> import Distribution.Simple++> main :: IO ()+> main = defaultMain

@@ -0,0 +1,32 @@+name:          eq+category:      Type System+version:       0.1.0+license:       BSD3+cabal-version: >= 1.2.3+license-file:  LICENSE+author:        Edward A. Kmett+maintainer:    Edward A. Kmett <ekmett@gmail.com>+stability:     provisional+homepage:      http://comonad.com/reader/+copyright:     Copyright (C) 2010-2011 Edward A. Kmett+synopsis:      Leibnizian equality+description:   Leibnizian equality+build-type:    Simple++flag TypeFamilies+  default: True++library+  build-depends: +    base >= 4 && < 5++  extensions: CPP++  if flag(TypeFamilies)+    cpp-options: -DLANGUAGE_TypeFamilies+    extensions: TypeFamilies++  exposed-modules:+    Data.Eq.Type++  ghc-options: -Wall