clean-unions (empty) → 0.0

raw patch · 4 files changed

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

Dependencies added: base

Files

LICENSE +30/−0
Setup.hs +2/−0
clean-unions.cabal +22/−0
src/Data/OpenUnion1/Clean.hs +82/−0

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2014, Fumiaki Kinoshita
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * 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.
+
+    * Neither the name of Fumiaki Kinoshita nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"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 COPYRIGHT
+OWNER 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.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple
+main = defaultMain

+ clean-unions.cabal view

@@ -0,0 +1,22 @@+name:                clean-unions
+version:             0.0
+synopsis:            Open unions without need for Typeable
+-- description:         
+homepage:            https://github.com/fumieval/clean-unions
+license:             BSD3
+license-file:        LICENSE
+author:              Fumiaki Kinoshita
+maintainer:          Fumiaki Kinoshita <fumiexcel@gmail.com>
+copyright:           Copyright (C) 2014 Fumiaki Kinoshita
+category:            Data
+build-type:          Simple
+-- extra-source-files:  
+cabal-version:       >=1.10
+
+library
+  exposed-modules:     Data.OpenUnion1.Clean
+  -- other-modules:       
+  other-extensions:    Rank2Types, TypeOperators, TypeFamilies, MultiParamTypeClasses, FlexibleInstances, DataKinds, KindSignatures, PolyKinds, GADTs, ScopedTypeVariables, LambdaCase, OverlappingInstances
+  build-depends:       base == 4.*
+  hs-source-dirs:      src
+  default-language:    Haskell2010

+ src/Data/OpenUnion1/Clean.hs view

@@ -0,0 +1,82 @@+{-# LANGUAGE Rank2Types
+  , TypeOperators
+  , TypeFamilies
+  , MultiParamTypeClasses
+  , FlexibleInstances
+  , DataKinds
+  , KindSignatures
+  , PolyKinds
+  , GADTs
+  , ScopedTypeVariables
+  , LambdaCase
+  , ConstraintKinds
+  , OverlappingInstances #-}
+module Data.OpenUnion1.Clean (Union, Nil, List(..), (|>)(..), (@>), exhaust, (∈)(), Member, liftU, (⊆)(..), Include) where
+import Data.Proxy
+
+-- | Poly-kinded list
+data List a = Empty | a :> List a
+
+infixr 5 :>
+infixr 5 |>
+
+-- | Append a new element to a union.
+type family (f :: * -> *) |> (s :: * -> *) :: * -> *
+
+type instance f |> Union s = Union (f :> s)
+
+-- | An uninhabited union.
+type Nil = Union Empty
+
+data family Union (s :: List (* -> *)) a
+
+data instance Union (f :> s) a = Single (f a) | Union (Union s a)
+data instance Union Empty a = Exhausted (Union Empty a)
+
+-- | Perform type-safe matching.
+(@>) :: (f x -> r) -- ^ first case
+  -> (Union s x -> r) -- ^ otherwise
+  -> (Union (f :> s) x -> r) -- ^ matching function
+(@>) run _ (Single f) = run f
+(@>) _ cont (Union r) = cont r
+infixr 0 @>
+
+exhaust :: Nil x -> m r
+exhaust (Exhausted a) = exhaust a
+
+data MemberInfo f s where
+  Head :: MemberInfo f (f :> s)
+  Tail :: (f ∈ s) => MemberInfo f (g :> s)
+
+-- | Constraint @f ∈ s@ indicates that @f@ is an element of a type-level list @s@.
+class f　∈ s where
+  query :: Proxy f -> Proxy s -> MemberInfo f s
+
+infix 4 ∈
+infix 4 ⊆
+
+instance f ∈ (f :> s) where query _ _ = Head
+instance (f　∈ s) => f　∈ (g :> s) where query _ _ = Tail
+
+-- | Lift some value into a union.
+liftU :: forall s f a. (f　∈ s) => f a -> Union s a
+liftU f = case query (Proxy :: Proxy f) (Proxy :: Proxy s) of
+  Head -> Single f
+  Tail -> Union (liftU f)
+
+-- | Type-level inclusion characterized by 'reunion'.
+class s　⊆ t where
+  -- | Lift a union into equivalent or larger one, permuting elements if necessary.
+  reunion :: Union s a -> Union t a
+
+instance (f ∈ t, s　⊆ t) => (f :> s)　⊆ t where
+  reunion (Single f) = liftU f
+  reunion (Union s) = reunion s
+
+-- | Every set has an empty set as its subset.
+instance Empty ⊆ t where
+  reunion = exhaust
+
+type Member f s = f ∈ s
+
+type Include s t = s ⊆ t