ty (empty) → 0.0.2

raw patch · 8 files changed

+184/−0 lines, 8 filesdep +basesetup-changed

Dependencies added: base

Files

• COPYING +25/−0
• Makefile +1/−0
• Setup.lhs +3/−0
• src/Data/IsTy.hs +21/−0
• src/Data/Proof/EQ.hs +50/−0
• src/Data/Ty.hs +39/−0
• ty.cabal +32/−0
• wikipage.tw +13/−0

@@ -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.+

@@ -0,0 +1,1 @@+include ../cho-home-cabal-make.inc

@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+> import Distribution.Simple+> main = defaultMain

@@ -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)

@@ -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

@@ -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)

@@ -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: <http://haskell.org/haskellwiki/ty>+  .+  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 

@@ -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 <tt>cabal install proof-eq</tt>.+* Get the code repository: <tt>http://code.haskell.org/~conal/code/applicative-numbers</tt>.+<!-- * See the [[proof-eq/Versions| version history]]. -->++<!-- Please leave comments at the [[Talk:proof-eq|Talk page]]. -->