packages feed

data-elevator (empty) → 0.1.0.0

raw patch · 5 files changed

+345/−0 lines, 5 filesdep +basedep +data-elevatordep +hspec

Dependencies added: base, data-elevator, hspec

Files

+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for data-elevator++## 0.1.0.0 -- 2022-07-31++* First version
+ data-elevator.cabal view
@@ -0,0 +1,61 @@+cabal-version:      2.4+name:               data-elevator+version:            0.1.0.0++tested-with: GHC ==9.2.3 || ==9.4.1++-- A short (one-line) description of the package.+synopsis: Coerce between unlifted boxed and lifted types.++-- A longer description of the package.+description: Near zero-cost coercions between unlifted boxed and lifted types.+             There are 3 main ingredients to this library:+             (1) a newtype @Strict :: LiftedType -> UnliftedType@,+             (2) a newtype @Lazy :: UnliftedType -> LiftedType@, and+             (3) a coercion function @levCoerce@ to coerce existing functions+                 into accepting @Strict@ wrapper.++-- The license under which the package is released.+license: MIT++-- The package author(s).+author: Sebastian Graf++-- An email address to which users can send suggestions, bug reports, and patches.+maintainer: sgraf1337@gmail.com++-- A copyright notice.+copyright: 2022+category: Data+extra-source-files: CHANGELOG.md++bug-reports: https://github.com/sgraf812/data-elevator/issues++source-repository head+  type: git+  location: https://github.com/sgraf812/data-elevator++library+    exposed-modules:  Data.Elevator+                      Data.Elevator.Internal++    -- Modules included in this library but not exported.+    -- other-modules:++    -- LANGUAGE extensions used by modules in this package.+    -- other-extensions:+    build-depends:    base ^>=4.16+    hs-source-dirs:   src+    default-language: Haskell2010++test-suite data-elevator-test+    default-language: Haskell2010+    type:             exitcode-stdio-1.0++    -- Directories containing source files.+    -- hs-source-dirs:+    main-is:          Main.hs+    hs-source-dirs:   test+    build-depends:    base ^>=4.16+                    , data-elevator+                    , hspec
+ src/Data/Elevator.hs view
@@ -0,0 +1,20 @@+-- | Near zero-cost coercions between lifted and boxed unlifted types.+--+-- Turn any lifted type into an unlifted boxed type with 'Strict', eagerly+-- forcing any wrapped computation in the syntactic binding context.+--+-- Turn any unlifted boxed type into a lifted type with 'Lazy', suspending any+-- wrapped computation until the 'Lazy' is matched upon.+--+-- Re-use existing code by coercing functions that can be generalised according+-- to the levity polymorphism subkinding law @Unlifted <: Lifted@ with+-- 'levCoerce'.++module Data.Elevator+  ( UnliftedType, LiftedType+  , Strict(Strict), Lazy(Lazy)+  , levCoerce, LevitySubsumption(..)+  ) where++import Data.Elevator.Internal+import GHC.Exts
+ src/Data/Elevator/Internal.hs view
@@ -0,0 +1,217 @@+{-# LANGUAGE BangPatterns          #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE RoleAnnotations       #-}+{-# LANGUAGE MagicHash             #-}+{-# LANGUAGE PatternSynonyms       #-}+{-# LANGUAGE ViewPatterns          #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE UnliftedNewtypes      #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE ExplicitForAll        #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE InstanceSigs          #-}++-- | This module doesn't respect the PVP!+-- Breaking changes may happen at any minor version (^>= *.*.m.*)++module Data.Elevator.Internal where++import GHC.Exts+import Data.Kind+import Unsafe.Coerce++-- | The kind of boxed, lifted types, for example @[Int]@ or any other+-- user-defined data type.+type LiftedType = Type++type U = UnliftedType+type L = LiftedType++type role Strict representational++-- | Turn a lifted data type into an unlifted one.+-- Unlifted data types enjoy a call-by-value calling convention. E.g.,+--+-- > let f :: (a :: UnliftedType) -> Int+-- >     f _ = 42+-- > in f (Strict (error "boom" :: Int))+--+-- Will error out with @"boom"@.+--+-- Note however that most function definitions don't take argument types of kind+-- 'UnliftedType'. Use 'levCoerce' to work around that.+newtype Strict (a :: LiftedType) where+  Strict_ :: Any @UnliftedType -> Strict a++toStrict# :: a -> Strict a+toStrict# = unsafeCoerce id++fromStrict# :: Strict a -> a+fromStrict# = unsafeCoerce id++pattern Strict :: a -> Strict a+pattern Strict x <- (fromStrict# -> x) where+  Strict x = toStrict# x+{-# INLINE Strict #-}+++type role Lazy representational++-- | Turn an unlifted boxed type into a lifted one.+-- @Lazy a@ then enjoys a call-by-name calling convention. E.g.,+--+-- > let f :: a -> Int+-- >     f _ = 42+-- > in f (Lazy (error "boom" :: Array# Int))+--+-- Will evaluate to @42@ and not error.+newtype Lazy (a :: UnliftedType) where+  Lazy_ :: Any @LiftedType -> Lazy a++toLazy# :: a -> Lazy a+toLazy# = unsafeCoerce id++fromLazy# :: Lazy a -> a+fromLazy# = unsafeCoerce id++pattern Lazy :: a -> Lazy a+pattern Lazy x <- (fromLazy# -> x) where+  Lazy x = toLazy# x+{-# INLINE Lazy #-}+++-- | Re-use existing code taking arguments lazily to take arguments 'Strict'ly+-- by coercing with 'levCoerce'.Example: 'even' can be+-- re-used on @Strict Int@:+--+-- >>> levCoerce @(Int -> Bool) @(Strict Int -> Bool) even (Strict 42)+-- True+--+-- More generally, any type of kind 'UnliftedType' can act as a (\"is-a\") type+-- of kind 'LiftedType'. This levity polymorphism subkinding axiom+-- @Unlifted <: Lifted@ is encoded in 'LevitySubsumption' and is lifted to+-- useful instances for 'Strict', 'Lazy' and '(->)'. Example with covariance in+-- the result type:+--+-- >>> levCoerce @(Int -> Strict Bool) @(Strict Int -> Bool) (\x -> Strict (even x)) (Strict 42)+-- True+--+-- A function from @Int@ to @Strict Bool@ can be called on a @Strict Int@ (e.g.,+-- the precondition strengthened) and the result can be coerced to @Bool@ (e.g.,+-- the postcondition weakened).+--+-- You can also keep on coercing in negative position of the function arrow,+-- with the variance following polarity:+--+-- > levCoerce @((Strict Int -> Int) -> Int)+-- >           @((Int -> Strict Int) -> Int)+-- >           (\f -> f (Strict 42))+-- >           (\x -> Strict x)+--+levCoerce :: LevitySubsumption a b => a -> b+levCoerce = levCoerce#++-- | Similar to 'Coercible', this type class models a subkinding relationship+-- between two types. The instances lift the @Unlifted <: Lifted@ sub-kinding+-- relationship to 'TYPE', 'Strict', 'Lazy' and then over function types.+--+-- Like for 'Coercible', the instances of this type class should ultimately be+-- compiler-generated.+class LevitySubsumption (a :: TYPE (BoxedRep l)) (b :: TYPE (BoxedRep r)) where+  levCoerce# :: a -> b++instance {-# OVERLAPPABLE #-} LevitySubsumption (a::LiftedType) a where+  levCoerce# x = x++instance {-# OVERLAPPABLE #-} LevitySubsumption (a::UnliftedType) a where+  levCoerce# x = x++instance {-# OVERLAPPING #-} LevitySubsumption (Strict a) a where+  levCoerce# (Strict a) = a++instance {-# OVERLAPPING #-} LevitySubsumption a (Lazy a) where+  levCoerce# a = Lazy a++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::L)) ((a2::L) -> (b2::L)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::L)) ((a2::L) -> (b2::U)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::L)) ((a2::U) -> (b2::L)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::L)) ((a2::U) -> (b2::U)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::U)) ((a2::L) -> (b2::L)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::U)) ((a2::L) -> (b2::U)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::U)) ((a2::U) -> (b2::L)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::L) -> (b1::U)) ((a2::U) -> (b2::U)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::L)) ((a2::L) -> (b2::L)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::L)) ((a2::L) -> (b2::U)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::L)) ((a2::U) -> (b2::L)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::L)) ((a2::U) -> (b2::U)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::U)) ((a2::L) -> (b2::L)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::U)) ((a2::L) -> (b2::U)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::U)) ((a2::U) -> (b2::L)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x++instance {-# OVERLAPPING #-} (LevitySubsumption a2 a1, LevitySubsumption b1 b2) => LevitySubsumption ((a1::U) -> (b1::U)) ((a2::U) -> (b2::U)) where+  -- Specification:+  -- > levCoerce# f x = levCoerce# (f (levCoerce# x :: a1))+  levCoerce# f x = unsafeCoerce# f x
+ test/Main.hs view
@@ -0,0 +1,42 @@+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE MagicHash        #-}++module Main where++import Data.Elevator.Internal+import Test.Hspec+import Control.Exception (evaluate, SomeException (SomeException))+import GHC.Exts++main :: IO ()+main = hspec $ do+  describe "Strict" $ do+    it "strict" $ do+      evaluate+        (let a = Strict (error "boom" :: Int)+             konst :: a -> Strict b -> a+             konst x y = x+        in konst 42 a)+        `shouldThrow` \(SomeException e) -> True++  describe "Lazy" $ do+    it "lazy" $ do+      (let a = Lazy (error "boom" :: Array# Int)+           konst :: a -> Lazy b -> a+           konst x y = x+       in konst 42 a)+      `shouldBe` 42++  describe "levCoerce" $ do+    describe "Refl" $ do+      it "Int ~ Int" $ do+        levCoerce @Int @Int 42 `shouldBe` (42 :: Int)+      it "Strict Int ~ Strict Int" $ do+        case levCoerce# @_ @_ @(Strict Int) @(Strict Int) (Strict 42) of Strict x -> x  `shouldBe` (42 :: Int)+    describe "->" $ do+      it "even" $ do+        levCoerce @(Int -> Bool) @(Strict Int -> Bool) even (Strict 42) `shouldBe` True+      it "co,contra: Int -> Strict Int ~ Int -> Strict Int" $ do+        levCoerce @(Int -> Strict Int) @(Strict Int -> Int) (\x -> Strict (x+1)) (Strict 42) `shouldBe` (43 :: Int)+      it "rank2 co: (Int -> Int) -> Int ~ (Strict Int -> Int) -> Int" $ do+        levCoerce @((Strict Int -> Int) -> Int) @((Int -> Strict Int) -> Int) (\f -> f (Strict 42)) (\x -> Strict x) `shouldBe` (42 :: Int)