diff --git a/COPYING b/COPYING new file mode 100644 --- /dev/null +++ b/COPYING @@ -0,0 +1,25 @@ +Copyright (c) 2009 Conal Elliott +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. The names of the authors may not 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 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. + diff --git a/Makefile b/Makefile new file mode 100644 --- /dev/null +++ b/Makefile @@ -0,0 +1,1 @@ +include ../cho-home-cabal-make.inc diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,3 @@ +#!/usr/bin/env runhaskell +> import Distribution.Simple +> main = defaultMain diff --git a/src/Data/IsTy.hs b/src/Data/IsTy.hs new file mode 100644 --- /dev/null +++ b/src/Data/IsTy.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -Wall #-} +---------------------------------------------------------------------- +-- | +-- Module : Data.IsTy +-- Copyright : (c) Conal Elliott 2009 +-- License : BSD3 +-- +-- Maintainer : conal@conal.net +-- Stability : experimental +-- +-- Type class for typed type representations +---------------------------------------------------------------------- + +module Data.IsTy (IsTy(..)) where + +import Data.Proof.EQ ((:=:)) + +-- | Type class for typed type representations +class IsTy ty where + tyEq :: ty a -> ty b -> Maybe (a :=: b) diff --git a/src/Data/Proof/EQ.hs b/src/Data/Proof/EQ.hs new file mode 100644 --- /dev/null +++ b/src/Data/Proof/EQ.hs @@ -0,0 +1,50 @@ +{-# LANGUAGE GADTs, KindSignatures, TypeOperators #-} +{-# OPTIONS_GHC -Wall #-} +---------------------------------------------------------------------- +-- | +-- Module : Data.Proof.EQ +-- Copyright : (c) Conal Elliott 2009 +-- License : BSD3 +-- +-- Maintainer : conal@conal.net +-- Stability : experimental +-- +-- Type equality proofs +---------------------------------------------------------------------- + +module Data.Proof.EQ + ( (:=:)(..) + , liftEq, liftEq2, liftEq3, liftEq4 + , commEq, transEq + ) where + +-- TODO: Maybe remove the Eq suffixes, since the module can be imported +-- qualified, plus unqualified import of '(:=:)(..)'. + +-- | Type equality proof +data (:=:) :: * -> * -> * where Refl :: a :=: a + +-- | Lift proof through a unary type constructor +liftEq :: a :=: a' -> f a :=: f a' +liftEq Refl = Refl + +-- | Lift proof through a binary type constructor (including '(,)') +liftEq2 :: a :=: a' -> b :=: b' -> f a b :=: f a' b' +liftEq2 Refl Refl = Refl + +-- | Lift proof through a ternary type constructor (including '(,,)') +liftEq3 :: a :=: a' -> b :=: b' -> c :=: c' -> f a b c :=: f a' b' c' +liftEq3 Refl Refl Refl = Refl + +-- | Lift proof through a quaternary type constructor (including '(,,,)') +liftEq4 :: a :=: a' -> b :=: b' -> c :=: c' -> d :=: d' + -> f a b c d :=: f a' b' c' d' +liftEq4 Refl Refl Refl Refl = Refl + +-- | Commutativity +commEq :: a :=: a' -> a' :=: a +commEq Refl = Refl + +-- | Transitivity +transEq :: a :=: a' -> a' :=: a'' -> a :=: a'' +transEq Refl Refl = Refl diff --git a/src/Data/Ty.hs b/src/Data/Ty.hs new file mode 100644 --- /dev/null +++ b/src/Data/Ty.hs @@ -0,0 +1,39 @@ +{-# LANGUAGE TypeOperators, ScopedTypeVariables #-} +{-# OPTIONS_GHC -Wall #-} +---------------------------------------------------------------------- +-- | +-- Module : Data.Ty +-- Copyright : (c) Conal Elliott 2009 +-- License : BSD3 +-- +-- Maintainer : conal@conal.net +-- Stability : experimental +-- +-- Typed typerefs +---------------------------------------------------------------------- + +module Data.Ty (Ty,tyRep,ty,tyOf,Typeable,module Data.IsTy) where + + +import Data.Typeable (Typeable,TypeRep,typeOf) +import Unsafe.Coerce (unsafeCoerce) + +import Data.Proof.EQ ((:=:)(..)) + +import Data.IsTy + +-- | Phantom type wrapper around a 'TypeRep' +data Ty a = Ty { tyRep :: TypeRep } + +instance Show (Ty a) where show = show . tyRep + +instance IsTy Ty where + Ty a `tyEq` Ty b | a == b = unsafeCoerce (Just Refl) + | otherwise = Nothing + +ty :: Typeable a => Ty a +ty = tyOf (undefined :: a) + +-- | The 'Ty' of a value +tyOf :: Typeable a => a -> Ty a +tyOf a = Ty (typeOf a) diff --git a/ty.cabal b/ty.cabal new file mode 100644 --- /dev/null +++ b/ty.cabal @@ -0,0 +1,32 @@ +Name: ty +Version: 0.0.2 +Cabal-Version: >= 1.2 +Synopsis: Typed type representations and equality proofs +Category: Data +Description: + Typed type representations and equality proofs + . + Project wiki page: + . + Copyright 2009 Conal Elliott; BSD3 license. +Author: Conal Elliott +Maintainer: conal@conal.net +Homepage: http://haskell.org/haskellwiki/ty +Package-Url: http://code.haskell.org/ty +Copyright: (c) 2009 by Conal Elliott +License: BSD3 +License-File: COPYING +Stability: experimental +build-type: Simple + +Library + hs-Source-Dirs: src + Extensions: + Build-Depends: base<5 + Exposed-Modules: + Data.Proof.EQ + Data.IsTy + Data.Ty + ghc-options: -Wall + +-- ghc-prof-options: -prof -auto-all diff --git a/wikipage.tw b/wikipage.tw new file mode 100644 --- /dev/null +++ b/wikipage.tw @@ -0,0 +1,13 @@ +[[Category:Packages]] + +== Abstract == + +'''proof-eq''' is a simple, one-module package for working with equality proofs. + +Besides this wiki page, here are more ways to find out about proof-eq: +* Visit the [http://hackage.haskell.org/cgi-bin/hackage-scripts/package/proof-eq Hackage page] for library documentation and to download & install. +* Or install with cabal install proof-eq. +* Get the code repository: http://code.haskell.org/~conal/code/applicative-numbers. + + +