kinds (empty) → 0.0.0.0

raw patch · 4 files changed

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

Dependencies added: base

Files

• LICENSE +25/−0
• Setup.lhs +4/−0
• kinds.cabal +34/−0
• src/Data/Kind.hs +108/−0

@@ -0,0 +1,25 @@+Copyright © 2009–2010 Brandenburgische Technische Universität Cottbus+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 the copyright holders nor the names of the 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 HOLDERS 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,4 @@+#!/usr/bin/env runghc++> import Distribution.Simple+> main = defaultMain

@@ -0,0 +1,34 @@+Name:          kinds+Version:       0.0.0.0+Cabal-Version: >= 1.2.3+Build-Type:    Simple+License:       BSD3+License-File:  LICENSE+Copyright:     © 2009–2010 Brandenburgische Technische Universität Cottbus+Author:        Wolfgang Jeltsch+Maintainer:    jeltsch@tu-cottbus.de+Stability:     provisional+Homepage:      http://community.haskell.org/~jeltsch/kinds/+Bug-Reports:   jeltsch@tu-cottbus.de+Package-URL:   http://hackage.haskell.org/packages/archive/kinds/0.0.0.0/kinds-0.0.0.0.tar.gz+Synopsis:      Emulation of subkinds and subkind polymorphism+Description:   Subkinds are the kind-level analog to subtypes. A kind denotes a set of types, and a+               subkind of some base kind denotes a subset of the base kind&#x2019;s set of types.+               Haskell has no support for subkinds and subkind polymorphism. However, this package+               can be used to emulate subkinds of kind&#xA0;@*@ and subkind variables.+               .+               To define a new subkind, the user declares a type that represents the subkind, and+               instantiates some classes. Afterwards, the user can declare types to be of that+               subkind and universally quantify over the inhabitants of the subkind. Since subkinds+               are represented by types, type-level polymorphism can be used to emulate kind-level+               polymorphism.+Category:      Type System+Tested-With:   GHC == 6.10.4++Library+    Build-Depends:   base >= 3.0 && < 4.1+    Extensions:      MultiParamTypeClasses+                     Rank2Types+                     TypeFamilies+    Exposed-Modules: Data.Kind+    HS-Source-Dirs:  src

@@ -0,0 +1,108 @@+{-|+    Support for subkinds, including subkind polymorphism.++    Imagine, we had a language extension for declaring subkinds where a subkind declaration would+    be written as follows:++    @+    subkind /K/ = /C_1/ => /t_1/ | ... | /C_n/ => /t_n/+    @++    Thereby, /K/ would be a kind identifier, the /t_i/ would be types and the /C_i/ would be+    contexts. This subkind declaration would introduce a subkind /K/ that covers all types that+    match one of the /t_i/ and fulfill the corresponding context. For example, the declaration++    @+    subkind Map = (Ord key) => Map key val | IntMap val+    @++    would declare the subkind @Map@ of all types whose values are maps. Note that the subkind @Map@+    would be different from the type @Map@.++    We will now see how a subkind declaration++    @+    subkind /K/ = /C_1/ => /t_1/ | ... | /C_n/ => /t_n/+    @++    can be emulated using this module. First, we declare an empty type @Kind/K/@ that+    represents the subkind. Then we add the following instance declaration:++    @+    instance Kind Kind/K/ where+     +        data All Kind/K/ item = All/K/ (forall /A_1/. /C_1/ => item /t_1/)+                                   ...+                                   (forall /A_n/. /C_n/ => item /t_n/)+     +        closed item = All/K/ item ... item+    @++    Thereby, each /A_i/ stands for a whitespace-separated sequence of the free variables+    of /t_i/. Finally, we add the following instance declaration for every /i/ between+    /1/ and /n/:++    @+    instance /C_i/ => Inhabitant Kind/K/ /t_i/ where+     +        specialize (All/K/ _ ... _ item _ ... _) = item+    @++    Thereby, the number of wildcard patterns before and after @item@ is /i - 1/ and /n - i/,+    respectively. The above subkind declaration for @Map@ can be emulated with the following code:++    @+    data KindMap+     +    instance Kind KindMap where+     +        data All KindMap item = AllMap (forall key val. (Ord key) => item (Map key val))+                                       (forall val.                  item (IntMap val))+     +        closed item = AllMap item item+     +    instance (Ord key) => Inhabitant KindMap (Map key val) where+     +        specialize (AllMap item _) = item+     +    instance Inhabitant KindMap (IntMap val) where+     +        specialize (AllMap _ item) = item+    @+-}+module Data.Kind (++    Kind (type All, closed),+    Inhabitant (specialize)++) where++    -- |The class of subkind representations.+    class Kind kind where++        {-|+            Universal quantification over the types of the subkind.++            For a subkind representation @Kind/K/@ of a subkind @/K/@ and a type @/f/@ of+            kind @* -> *@, @All Kind/K/ /f/@ is isomorphic to @forall a :: /K/. /f/ a@.+        -}+        data All kind :: (* -> *) -> *++        {-|+            Conversion from a type that uses normal universal quantification into one that uses+            subkind-specific universal quantification.+        -}+        closed :: (forall inhabitant. (Inhabitant kind inhabitant) => item inhabitant) ->+                  All kind item++    -- |Specifies what types are inhabitants of what subkinds.+    class (Kind kind) => Inhabitant kind inhabitant where++        {-|+            Conversion from a universally quantified type into a type that is fixed to a specific+            inhabitant.++            This method exists to ensure that one cannot extend the subkind. If one would try to add+            a new inhabitant, one would have to provide an implementation of @specialize@.+        -}+        specialize :: All kind item -> item inhabitant