coercible-subtypes (empty) → 0.1.0.0

raw patch · 7 files changed

+342/−0 lines, 7 filesdep +basedep +profunctorssetup-changed

Dependencies added: base, profunctors

Files

CHANGELOG.md +5/−0
LICENSE +30/−0
README.md +107/−0
Setup.hs +2/−0
coercible-subtypes.cabal +35/−0
src/Data/Type/Coercion/Sub.hs +121/−0
src/Data/Type/Coercion/Sub/Internal.hs +42/−0

+ CHANGELOG.md view

@@ -0,0 +1,5 @@+# Revision history for coercible-subtypes++## 0.1.0.0 -- 2020-04-08++* First version.

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2020, Koji Miyazato++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 Koji Miyazato 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.

+ README.md view

@@ -0,0 +1,107 @@+# coercible-subtypes++This library provides unidirectional (one-way) variant of [Coercion](https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Type-Coercion.html).++The variant is a type `Sub` defined in `Data.Type.Coercion.Sub`.+`Sub a b` can be used to convert a type `a` to another type `b`.++```+upcastWith :: Sub a b -> a -> b+```++For all `Sub a b` values, the runtime representation of `a` and+`b` values are same, so `upcastWith` do not require any computation+to return `b` value, just [coerce](https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Coerce.html)s+GHC to treat a value of `a` as type `b`.+This feature is not different to `Coercion`.++The difference is that while `Coercion` represents+bidirectional relation, `Sub` represents unidirectional relation.+`Coercion a b` and its underlying type class `Coercible a b` witnesse you can coerce both `a` to `b` and `b` to `a`.+Unlike that, `Sub a b` only allows you to coerce `a` to `b`, not `b` to `a`.++## Usage Example++To use this library effectively, it must be used at two places: a library+and its user code. For this example, let's assume they are written by two people,+a *library author* and a *user*.++The library author writes a module `RightTriangle` below.++```+module RightTriangle(Triangle(), toEdges, getEdges, fromEdges) where+  import Data.Coerce+  import Data.Type.Coercion.Sub+  +  newtype Triangle = MkTriangle (Int, Int, Int)+  +  -- | Triangles can be coerced into 3-tuples of Ints+  toEdges :: Sub Triangle (Int, Int, Int)+  toEdges = sub+  +  getEdges :: Triangle -> (Int, Int, Int)+  getEdges = coerce+  +  -- | Creates right triangle from lengths of edges (a,b,c)+  -- +  -- >  *+  -- >  |\ c+  -- > a| \+  -- >  *--*+  -- >   b+  --+  -- (a^2 + b^2 == c^2) must hold.+  fromEdges :: (Int, Int, Int) -> Maybe Triangle+  fromEdges = {- Omit -}+```++The author wants to protect the invariant condition `a^2 + b^2 == c^2`.+For that purpose, the author can't export the constructor of `Triangle`.+Because it is symmetric, `Coercion Triangle (Int,Int,Int)` can't be exported either.++The user is building an application using `RightTriangle` module.++```+module Main where+  import Data.Map (Map)+  import RightTriangle+  +  import Data.Type.Coercion.Sub+  +  main :: IO ()+  main = ......+```++In this application, the user has to convert `Map String Triangle` to+`Map String (Int, Int, Int)`, revealing the edge lengths of the triangles.+While it is easy to do so with `fmap getEdges`,+using `fmap` here can make an entire copy of the Map<sup>[†](#footnote)</sup>.+This is wasted work and memory. Instead, the user can use `mapR toEdges` to get+`Sub (Map String Triangle) (Map String (Int, Int, Int))`+and then `upcastWith` to perform zero cost coercion over `Map`.++## Comparison against other methods++There are some other methods to achive the goal of this library.++* Just give up coercion++  * This is just for better performance, so not doing it+    is always an option.++* Rewrite rules++  * Rewrite rules based method is currently employed, and working at our hand.+    So, it is possible you don't need this library at all.+  +  * The downside is whether it works or not is on the provider of the+    "container" type in use, and GHC doing expected optimizations.+    Without reading source codes and examining the GHC optimization result (e.g. `-ddump-rule-firings`),+    you can't be sure you are doing the conversion zero-cost.++--------++<a id="footnote">†</a> For `Data.Map`, which [containers](https://hackage.haskell.org/package/containers)+package provides, can optimize `fmap` away via proper inlining and rewrite rules. The purpose of this library+is turning optimizations into explicit codes, or handling the cases when the container type in use does not+provide such an opportunity via rewrite rules.</small>

+ Setup.hs view

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

+ coercible-subtypes.cabal view

@@ -0,0 +1,35 @@+cabal-version:       2.2+name:                coercible-subtypes+version:             0.1.0.0+stability:           experimental+synopsis:            Coercible but only in one direction+description: Newtype wrapper 'Data.Type.Coercion.Sub.Sub'+             around 'Data.Type.Coercion.Coercion'+             to represent unidirectional coercion,+             and combinators for it, like 'Data.Type.Coercion.Sub.mapR'+             which extends coercion over covariant @Functor@.++homepage:            https://github.com/viercc/coercible-subtypes+bug-reports:         https://github.com/viercc/coercible-subtypes/issues+license:             BSD-3-Clause+license-file:        LICENSE+author:              Koji Miyazato+maintainer:          viercc@gmail.com+copyright:           (c) 2020 Koji Miyazato+category:            Data+build-type:          Simple+extra-source-files:  CHANGELOG.md, README.md++source-repository HEAD+  type:     git+  location: https://github.com/viercc/coercible-subtypes+  branch:   master++library+  exposed-modules:     Data.Type.Coercion.Sub,+                       Data.Type.Coercion.Sub.Internal+  build-depends:       base >=4.12 && <4.15,+                       profunctors+  hs-source-dirs:      src+  default-language:    Haskell2010+  ghc-options:         -Wall -Wcompat

+ src/Data/Type/Coercion/Sub.hs view

@@ -0,0 +1,121 @@+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes            #-}+module Data.Type.Coercion.Sub(+  {- | @Sub a b@ witnesses a zero-cost conversion @a -> b@.++  @Sub@ is a newtype wrapper around 'Coercion', but made opaque to hide+  the ability to 'Data.Coerce.coerce' into other direction.++  This is convenient for newtype wrappers which give additional guarantees.++  As an example, think about the following code:++  > -- | A pair @(x::a, y::a)@, but guaranteed @x <= y@+  > newtype Range a = MkRange (a,a)+  >+  > getRange :: Range a -> (a,a)+  > getRange = coerce+  > mkRange :: Ord a => a -> a -> Range a+  > mkRange x y = if x <= y then MkRange (x,y) else MkRange (y,x)++  If you want to provide this type from a library you maintain,+  you would want to keep @Range@ abstract from outside of the module.++  An user may want to convert @[Range a]@ to @[(a,a)]@ without actually+  traversing the list. This is possible if the user have access to the+  internals, or you export a @Coercion (Range a) (a,a)@ value. But doing so+  breaks the guarantee, because it also allows to use @Coercible@ in the other+  direction, as in @coerce (10,5) :: Range Int@.++  By exporting only @Sub (Range a) (a,a)@ value from your module,+  this user can get @Sub [Range a] [(a,a)]@ using 'mapR',+  without being able to make an invalid value.+  +  -}+  Sub(),+  sub, toSub, upcastWith, equiv, gequiv,++  coercionIsSub,++  mapR, contramapR,+  bimapR, dimapR+) where++import           Data.Coerce+import           Data.Type.Coercion++import           Data.Bifunctor                  (Bifunctor)+import           Data.Functor.Contravariant      (Contravariant)+import           Data.Profunctor                 (Profunctor)++import           Data.Type.Coercion.Sub.Internal++-- | Make a witness for type-safe casting which respects direction.+sub :: Coercible a b => Sub a b+sub = Sub Coercion++toSub :: Coercion a b -> Sub a b+toSub = Sub++-- | Type-safe cast+upcastWith :: Sub a b -> a -> b+upcastWith (Sub Coercion) = coerce++-- | All 'Coercion' can be seen as 'Sub'+coercionIsSub :: Sub (Coercion a b) (Sub a b)+coercionIsSub = Sub Coercion++-- | `Sub` relation in both direction means there is `Coercion` relation.+equiv :: Sub a b -> Sub b a -> Coercion a b+equiv ab ba = gequiv ab ba Coercion++-- | Generalized 'equiv'+gequiv :: Sub a b -> Sub b a -> (Coercible a b => r) -> r+gequiv (Sub Coercion) (Sub Coercion) k = k++{-++Note: evaluating both arguments of `equiv` is necessary.+One might notice the following typechecks.++    equiv :: Sub a b -> Sub b a -> Coercion a b+    equiv (Sub Coercion) _ = Coercion++But this implementation allows inverting `Sub a b` circumventing the restriction;++    bad :: Sub a b -> Sub b a+    bad ab =+      let ba = upcastWith coercionIsSub (equiv ab ba)+      in ba++This is prevented by evaluating both arguments of `equiv`, making `bad ab` a bottom.++-}++-----------------------------++-- | Extend subtype relation covariantly.+mapR :: ( forall x x'. Coercible x x' => Coercible (t x) (t x')+        , Functor t)+     => Sub a b -> Sub (t a) (t b)+mapR (Sub Coercion) = Sub Coercion++-- | Extend subtype relation contravariantly+contramapR :: ( forall x x'. Coercible x x' => Coercible (t x) (t x')+              , Contravariant t)+           => Sub a b -> Sub (t b) (t a)+contramapR (Sub Coercion) = Sub Coercion++bimapR :: ( forall x x' y y'.+              (Coercible x x', Coercible y y') => Coercible (t x y) (t x' y')+          , Bifunctor t)+       => Sub a a' -> Sub b b' -> Sub (t a b) (t a' b')+bimapR (Sub Coercion) (Sub Coercion) = Sub Coercion++dimapR :: ( forall x x' y y'.+              (Coercible x x', Coercible y y') => Coercible (t x y) (t x' y')+          , Profunctor t)+       => Sub a a' -> Sub b b' -> Sub (t a' b) (t a b')+dimapR (Sub Coercion) (Sub Coercion) = Sub Coercion

+ src/Data/Type/Coercion/Sub/Internal.hs view

@@ -0,0 +1,42 @@+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE InstanceSigs          #-}+{-# LANGUAGE PolyKinds             #-}++{- |++This module exposes internals of "Data.Type.Coercion.Sub".++Using this module allows to violate the premises 'Sub' type provides.+It is advisable not to import this module if there is another way,+and to limit the amount of code accesible to this module.++-}+module Data.Type.Coercion.Sub.Internal(+  Sub(..)+) where++import           Control.Category+import           Prelude                    hiding (id, (.))++import           Data.Type.Coercion++newtype Sub (a :: k) (b :: k) = Sub { getSub :: Coercion a b }+  deriving (Eq, Ord, Show)+-- It is intentional to omit some instances.+--+-- TestCoercion instance should not exist.+-- Knowing `Sub a b` and `Sub a c` should not conclude+-- `Coercible b c`.+--+-- Among instances `Coercion` has, Enum, Bounded, and Read are+-- excluded because they allows to make new value of `Sub a b`.+-- Constructing `Sub a b` values must be done through+-- combinators provided by this module or exported for+-- abstract type under library author's careful choice.++instance Category Sub where+  id :: Sub a a+  id = Sub Coercion++  (.) :: Sub b c -> Sub a b -> Sub a c+  Sub Coercion . Sub Coercion = Sub Coercion