diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,4 @@ +#!/usr/bin/env runghc + +> import Distribution.Simple +> main = defaultMain diff --git a/kinds.cabal b/kinds.cabal new file mode 100644 --- /dev/null +++ b/kinds.cabal @@ -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’s set of types. + Haskell has no support for subkinds and subkind polymorphism. However, this package + can be used to emulate subkinds of kind @*@ 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 diff --git a/src/Data/Kind.hs b/src/Data/Kind.hs new file mode 100644 --- /dev/null +++ b/src/Data/Kind.hs @@ -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