packages feed

records-sop (empty) → 0.1.0.0

raw patch · 7 files changed

+629/−0 lines, 7 filesdep +basedep +deepseqdep +generics-sopsetup-changed

Dependencies added: base, deepseq, generics-sop, ghc-prim, hspec, records-sop, should-not-typecheck

Files

+ CHANGELOG.md view
@@ -0,0 +1,8 @@+# 0.1.0.0 (2017-05-01)++* Initial release. Everything is still rather experimental.+  Feedback on any aspect of the library is welcome.++  Currently, the general utilities are in+  `Generics.SOP.Record`, and the subtyping functionality is+  in `Generics.SOP.Record.SubTyping`.
+ LICENSE view
@@ -0,0 +1,27 @@+Copyright (c) 2017, Andres Löh+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice,+   this list of conditions and the following disclaimer.++2. 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.++3. Neither the name of the copyright holder nor the names of its 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 HOLDER 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
+ records-sop.cabal view
@@ -0,0 +1,58 @@+name: records-sop+version: 0.1.0.0+author: Andres Löh <andres@well-typed.com>+maintainer: andres@well-typed.com+license: BSD3+license-file: LICENSE+cabal-version: >= 1.10+build-type: Simple+tested-with: GHC == 8.0.1, GHC == 8.0.2, GHC == 8.2.1, GHC == 8.3.*+category: Generics+synopsis: Record subtyping and record utilities with generics-sop+description:+  This library provides utilities for working with labelled+  single-constructor record types via generics-sop.+  .+  It also provides functions to safely cast between record+  types if the target type has a subset of the fields (with+  the same names) of the source type.+extra-source-files: CHANGELOG.md++source-repository head+  type: git+  location: https://github.com/kosmikus/records-sop++library+  hs-source-dirs:+    src+  ghc-options:+    -Wall+  exposed-modules:+    Generics.SOP.Record,+    Generics.SOP.Record.SubTyping+  build-depends:+    base >= 4.9 && < 5.0,+    deepseq >= 1.3 && < 1.5,            +    generics-sop >= 0.3 && < 0.4,+    ghc-prim >= 0.5 && < 0.6+  default-language:+    Haskell2010++test-suite examples+  type:+    exitcode-stdio-1.0+  hs-source-dirs:+    tests+  ghc-options:+    -Wall+  main-is:+    Examples.hs+  build-depends:+    base >= 4.9 && < 5.0,+    deepseq >= 1.4 && < 1.5,+    hspec >= 2.2 && < 2.5,+    generics-sop >= 0.3 && < 0.4,+    records-sop,+    should-not-typecheck >= 2.1 && < 2.2+  default-language:+    Haskell2010
+ src/Generics/SOP/Record.hs view
@@ -0,0 +1,275 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}+module Generics.SOP.Record+  ( -- * A suitable representation for single-constructor records+    FieldLabel+  , RecordCode+  , Record+  , RecordRep+    -- * Computing the record code+  , RecordCodeOf+  , IsRecord+  , ValidRecordCode+  , ExtractTypesFromRecordCode+  , ExtractLabelsFromRecordCode+  , RecombineRecordCode+    -- * Conversion between a type and its record representation.+  , toRecord+  , fromRecord+    -- * Utilities+  , P(..)+  , Snd+  )+  where++import Control.DeepSeq+import Generics.SOP.BasicFunctors+import Generics.SOP.NP+import Generics.SOP.NS+import Generics.SOP.Universe+import Generics.SOP.Sing+import Generics.SOP.Type.Metadata+import qualified GHC.Generics as GHC+import GHC.TypeLits+import GHC.Types+import Unsafe.Coerce++--------------------------------------------------------------------------+-- A suitable representation for single-constructor records.+--------------------------------------------------------------------------++-- | On the type-level, we represent fiel labels using symbols.+type FieldLabel = Symbol++-- | The record code deviates from the normal SOP code in two+-- ways:+--+-- - There is only one list, because we require that there is+--   only a single constructor.+--+-- - In addition to the types of the fields, we store the labels+--   of the fields.+--+type RecordCode = [(FieldLabel, Type)]++-- | The record representation of a type is a record indexed+-- by the record code.+--+type RecordRep (a :: Type) = Record (RecordCodeOf a)++-- | The representation of a record is just a product indexed by+-- a record code, containing elements of the types indicated+-- by the code.+--+-- Note that the representation is deliberately chosen such that+-- it has the same run-time representation as the product part+-- of the normal SOP representation.+--+type Record (r :: RecordCode) = NP P r++--------------------------------------------------------------------------+-- Computing the record code+--------------------------------------------------------------------------++-- | This type-level function takes the type-level metadata provided+-- by generics-sop as well as the normal generics-sop code, and transforms+-- them into the record code.+--+-- Arguably, the record code is more usable than the representation+-- directly on offer by generics-sop. So it's worth asking whether+-- this representation should be included in generics-sop ...+--+-- The function will only reduce if the argument type actually is a+-- record, meaning it must have exactly one constructor, and that+-- constructor must have field labels attached to it.+--+type RecordCodeOf a = ToRecordCode_Datatype a (DatatypeInfoOf a) (Code a)++-- | Helper for 'RecordCodeOf', handling the datatype level. Both+-- datatypes and newtypes are acceptable. Newtypes are just handled+-- as one-constructor datatypes for this purpose.+--+type family+  ToRecordCode_Datatype (a :: Type) (d :: DatatypeInfo) (c :: [[Type]]) :: RecordCode where+  ToRecordCode_Datatype a (ADT _ _ cis)    c = ToRecordCode_Constructor a cis c+  ToRecordCode_Datatype a (Newtype _ _ ci) c = ToRecordCode_Constructor a '[ ci ] c++-- | Helper for 'RecordCodeOf', handling the constructor level. Only+-- single-constructor types are acceptable, and the constructor must+-- contain field labels.+--+-- As an exception, we accept an empty record, even though it does+-- not explicitly define any field labels.+--+type family+  ToRecordCode_Constructor (a :: Type) (cis :: [ConstructorInfo]) (c :: [[Type]]) :: RecordCode where+  ToRecordCode_Constructor a '[ 'Record _ fis  ] '[ ts  ] = ToRecordCode_Field fis ts+  ToRecordCode_Constructor a '[ 'Constructor _ ] '[ '[] ] = '[]+  ToRecordCode_Constructor a '[]                  _       =+    TypeError+      (    Text "The type `" :<>: ShowType a :<>: Text "' is not a record type."+      :$$: Text "It has no constructors."+      )+  ToRecordCode_Constructor a ( _ : _ : _ )        _       =+    TypeError+      (    Text "The type `" :<>: ShowType a :<>: Text "' is not a record type."+      :$$: Text "It has more than one constructor."+      )+  ToRecordCode_Constructor a '[ _ ]               _       =+    TypeError+      (    Text "The type `" :<>: ShowType a :<>: Text "' is not a record type."+      :$$: Text "It has no labelled fields."+      )++-- | Helper for 'RecordCodeOf', handling the field level. At this point,+-- we simply zip the list of field names and the list of types.+--+type family ToRecordCode_Field (fis :: [FieldInfo]) (c :: [Type]) :: RecordCode where+  ToRecordCode_Field '[]                    '[]        = '[]+  ToRecordCode_Field ( 'FieldInfo l : fis ) ( t : ts ) = '(l, t) : ToRecordCode_Field fis ts++-- * Relating the record code and the original code.++-- | The constraint @IsRecord a r@ states that the type 'a' is a record type+-- (i.e., has exactly one constructor and field labels) and that 'r' is the+-- record code associated with 'a'.+--+type IsRecord (a :: Type) (r :: RecordCode) =+  IsRecord' a r (GetSingleton (Code a))++-- | The constraint @IsRecord' a r xs@ states that 'a' is a record type+-- with record code 'r', and that the types contained in 'r' correspond+-- to the list 'xs'.+--+-- If the record code computation is correct, then the record code of a+-- type is strongly related to the original generics-sop code. Extracting+-- the types out of 'r' should correspond to 'xs'. Recombining the+-- labels from 'r' with 'xs' should yield 'r' exactly. These sanity+-- properties are captured by 'ValidRecordCode'.+--+type IsRecord' (a :: Type) (r :: RecordCode) (xs :: [Type]) =+  ( Generic a, Code a ~ '[ xs ]+  , RecordCodeOf a ~ r, ValidRecordCode r xs+  )++-- | Relates a recordcode 'r' and a list of types 'xs', stating that+-- 'xs' is indeed the list of types contained in 'r'.+--+type ValidRecordCode (r :: RecordCode) (xs :: [Type]) =+  ( ExtractTypesFromRecordCode r ~ xs+  , RecombineRecordCode (ExtractLabelsFromRecordCode r) xs ~ r+  )++-- | Extracts all the types from a record code.+type family ExtractTypesFromRecordCode (r :: RecordCode) :: [Type] where+  ExtractTypesFromRecordCode '[]             = '[]+  ExtractTypesFromRecordCode ( '(_, a) : r ) = a : ExtractTypesFromRecordCode r++-- | Extracts all the field labels from a record code.+type family ExtractLabelsFromRecordCode (r :: RecordCode) :: [FieldLabel] where+  ExtractLabelsFromRecordCode '[]             = '[]+  ExtractLabelsFromRecordCode ( '(l, _) : r ) = l : ExtractLabelsFromRecordCode r++-- | Given a list of labels and types, recombines them into a record code.+--+-- An important aspect of this function is that it is defined by induction+-- on the list of types, and forces the list of field labels to be at least+-- as long.+--+type family RecombineRecordCode (ls :: [FieldLabel]) (ts :: [Type]) :: RecordCode where+  RecombineRecordCode _ '[]       = '[]+  RecombineRecordCode ls (t : ts) = '(Head ls, t) : RecombineRecordCode (Tail ls) ts++--------------------------------------------------------------------------+-- Conversion between a type and its record representation.+--------------------------------------------------------------------------++-- | Convert a value into its record representation.+toRecord :: (IsRecord a _r) => a -> RecordRep a+toRecord = unsafeToRecord_NP . unZ . unSOP . from++-- | Convert an n-ary product into the corresponding record+-- representation. This is a no-op, and more efficiently+-- implented using 'unsafeToRecord_NP'. It is included here+-- to demonstrate that it actually is type-correct and also+-- to make it more obvious that it is indeed a no-op.+--+_toRecord_NP :: (ValidRecordCode r xs) => NP I xs -> Record r+_toRecord_NP Nil         = Nil+_toRecord_NP (I x :* xs) = P x :* _toRecord_NP xs++-- | Fast version of 'toRecord_NP'. Not actually unsafe as+-- long as the internal representations of 'NP' and 'Record'+-- are not changed.+--+unsafeToRecord_NP :: (ValidRecordCode r xs) => NP I xs -> Record r+unsafeToRecord_NP = unsafeCoerce++-- | Convert a record representation back into a value.+fromRecord :: (IsRecord a r) => RecordRep a -> a+fromRecord = to . SOP . Z . unsafeFromRecord_NP++-- | Convert a record representation into an n-ary product. This is a no-op,+-- and more efficiently implemented using 'unsafeFromRecord_NP'.+--+-- It is also noteworthy that we let the resulting list drive the computation.+-- This is compatible with the definition of 'RecombineRecordCode' based on+-- the list of types.+--+_fromRecord_NP :: forall r xs . (ValidRecordCode r xs, SListI xs) => Record r -> NP I xs+_fromRecord_NP = case sList :: SList xs of+  SNil  -> const Nil+  SCons -> \ r -> case r of+    P x :* xs -> I x :* _fromRecord_NP xs++-- | Fast version of 'fromRecord_NP'. Not actually unsafe as+-- long as the internal representation of 'NP' and 'Record'+-- are not changed.+--+unsafeFromRecord_NP :: forall r xs . (ValidRecordCode r xs, SListI xs) => Record r -> NP I xs+unsafeFromRecord_NP = unsafeCoerce++--------------------------------------------------------------------------+-- Utilities+--------------------------------------------------------------------------+ +-- | Projection of the second component of a type-level pair,+-- wrapped in a newtype.+--+newtype P (p :: (a, Type)) = P (Snd p)+  deriving (GHC.Generic)++deriving instance Eq a => Eq (P '(l, a))+deriving instance Ord a => Ord (P '(l, a))+deriving instance Show a => Show (P '(l, a))++instance NFData a => NFData (P '(l, a)) where+  rnf (P x) = rnf x++-- | Type-level variant of 'snd'.+type family Snd (p :: (a, b)) :: b where+  Snd '(a, b) = b++-- | Type-level variant of 'head'.+type family Head (xs :: [k]) :: k where+  Head (x : xs) = x++-- | Type-level variant of 'tail'.+type family Tail (xs :: [k]) :: [k] where+  Tail (x : xs) = xs++-- | Partial type-level function that extracts the only element+-- from a singleton type-level list.+--+type family GetSingleton (xs :: [k]) :: k where+  GetSingleton '[ x ] = x
+ src/Generics/SOP/Record/SubTyping.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE+    AllowAmbiguousTypes+  , FlexibleInstances+  , MultiParamTypeClasses+  , ScopedTypeVariables+  , TypeApplications+  , TypeInType+  , TypeFamilies+  , TypeOperators+  , UndecidableInstances+#-}+{-# OPTIONS_GHC+  -fno-warn-unticked-promoted-constructors+#-}+module Generics.SOP.Record.SubTyping+  ( cast+  , IsSubTypeOf+  , IsElemOf+  )+  where++import Data.Type.Equality+import Generics.SOP.NP+import GHC.Types++import Generics.SOP.Record++-- | Cast one record type to another if there is a subtype relationship+-- between them. Currently, only width subtyping is considered, which means+-- that we can forget and reorder fields.+--+cast :: (IsRecord a ra, IsRecord b rb, IsSubTypeOf ra rb) => a -> b+cast = fromRecord . castRecord . toRecord++-- | Class that checks whether one record code is convertible into another.+--+-- Conversion works if the first record contains at least the labels of the+-- second record, and if the types of the corresponding fields match exactly.+--+class IsSubTypeOf (r1 :: RecordCode) (r2 :: RecordCode) where+  -- | Perform a safe cast between two records.+  castRecord :: Record r1 -> Record r2++instance IsSubTypeOf r1 '[] where+  castRecord _ = Nil++instance (IsSubTypeOf r1 r2, IsElemOf s2 a2 r1) => IsSubTypeOf r1 ( '(s2, a2) : r2 ) where+  castRecord r = P (get @s2 r) :* castRecord r++-- | Class that checks whether a field of a particular type is contained+-- in a record.+--+class IsElemOf (s :: Symbol) (a :: Type) (r :: RecordCode) where+  -- | Perform an extraction of a given field. Field name has to be passed+  -- via type application.+  --+  get :: Record r -> a++-- | Helper class. Isn't strictly needed, but allows us to avoid+-- overlapping instances for the 'IsElemOf' class.+--+class IsElemOf' (b :: Bool)+  (s1 :: FieldLabel) (a1 :: Type)+  (s2 :: FieldLabel) (a2 :: Type)+  (r :: RecordCode)+  where+  get' :: Record ( '(s2, a2) : r ) -> a1++instance+  IsElemOf' (SameFieldLabel s1 s2) s1 a1 s2 a2 r =>+  IsElemOf s1 a1 ( '(s2, a2) : r )+  where+  get = get' @(SameFieldLabel s1 s2) @s1++instance (a1 ~ a2) => IsElemOf' True s a1 s a2 r where+  get' (P a :* _) = a++instance IsElemOf s1 a1 r => IsElemOf' False s1 a1 s2 a2 r where+  get' (_ :* r) = get @s1 r++-- | Decide the equality of two field labels.+--+-- Just a special case of polymorphic type equality.+--+type family+  SameFieldLabel (s1 :: FieldLabel) (s2 :: FieldLabel) :: Bool where+  SameFieldLabel s1 s2 = s1 == s2
+ tests/Examples.hs view
@@ -0,0 +1,172 @@+{-# LANGUAGE+    DeriveGeneric+  , DuplicateRecordFields+#-}+{-# OPTIONS_GHC -fdefer-type-errors -Wno-deferred-type-errors #-}+module Main where++import Control.DeepSeq+import qualified GHC.Generics as GHC+import Test.Hspec+import Test.ShouldNotTypecheck++import Generics.SOP+import Generics.SOP.Record+import Generics.SOP.Record.SubTyping++data X = MkX {}+  deriving (Eq, Show, GHC.Generic)++instance Generic X+instance HasDatatypeInfo X+instance NFData X++data A = MkA { anInt :: Int, aBool :: Bool }+  deriving (Eq, Show, GHC.Generic)++instance Generic A+instance HasDatatypeInfo A+instance NFData A++data B = MkB { anInt :: Int, aBool :: Bool, aChar :: Char }+  deriving (Eq, Show, GHC.Generic)++instance Generic B+instance HasDatatypeInfo B+instance NFData B++-- Permutation.+data C = MkC { aBool :: Bool, aChar :: Char, anInt :: Int }+  deriving (Eq, Show, GHC.Generic)++instance Generic C+instance HasDatatypeInfo C+instance NFData C++-- Duplicate label within a single record (works!).+data D = MkD { anInt :: Int, anInt :: Int }+  deriving (Eq, Show, GHC.Generic)++instance Generic D+instance HasDatatypeInfo D+instance NFData D++-- Wrong type.+data E = MkE { anInt :: Int, aBool :: Bool, aChar :: () }+  deriving (Eq, Show, GHC.Generic)++instance Generic E+instance HasDatatypeInfo E+instance NFData E++-- No field labels.+data F = MkF Int Bool Char+  deriving (Eq, Show, GHC.Generic)++instance Generic F+instance HasDatatypeInfo F+instance NFData F++-- Two constructors.+data G = MkG { anInt :: Int, aBool :: Bool, aChar :: Char }+       | OtherG+  deriving (Eq, Show, GHC.Generic)++instance Generic G+instance HasDatatypeInfo G+instance NFData G++a :: A+a = MkA 3 True++b :: B+b = MkB 3 True 'x'++c :: C+c = MkC True 'x' 3++d :: D+d = MkD 3 3++d' :: D+d' = MkD 3 4++e :: E+e = MkE 3 True ()++f :: F+f = MkF 3 True 'x'++g :: G+g = MkG 3 True 'x'++x :: X+x = MkX {}++main :: IO ()+main = hspec $+  describe "cast" $ do+    it "successfully casts X to X" $+      (cast x :: X) `shouldBe` x+    it "successfully casts A to A" $+      (cast a :: A) `shouldBe` a+    it "successfully casts A to X" $+      (cast a :: X) `shouldBe` x+    it "successfully casts A to D" $+      (cast a :: D) `shouldBe` d+    it "successfully casts B to B" $+      (cast b :: B) `shouldBe` b+    it "successfully casts B to X" $+      (cast b :: X) `shouldBe` x+    it "successfully casts B to A" $+      (cast b :: A) `shouldBe` a+    it "successfully casts B to C" $+      (cast b :: C) `shouldBe` c+    it "successfully casts B to D" $+      (cast b :: D) `shouldBe` d+    it "successfully casts C to X" $+      (cast c :: X) `shouldBe` x+    it "successfully casts C to A" $+      (cast c :: A) `shouldBe` a+    it "successfully casts C to B" $+      (cast c :: B) `shouldBe` b+    it "successfully casts C to D" $+      (cast c :: D) `shouldBe` d+    it "successfully casts D to D" $+      (cast d :: D) `shouldBe` d+    it "prefers the first element when casting D to D" $+      (cast d' :: D) `shouldBe` d+    it "successfully casts D to X" $+      (cast d :: X) `shouldBe` x+    it "successfully casts E to E" $+      (cast e :: E) `shouldBe` e+    it "successfully casts E to X" $+      (cast e :: X) `shouldBe` x+    it "successfully casts E to A" $+      (cast e :: A) `shouldBe` a+    it "successfully casts E to D" $+      (cast e :: D) `shouldBe` d+    it "correctly fails to cast A to B" $+      shouldNotTypecheck (cast a :: B)+    it "correctly fails to cast A to C" $+      shouldNotTypecheck (cast a :: C)+    it "correctly fails to cast D to A" $+      shouldNotTypecheck (cast d :: A)+    it "correctly fails to cast D to B" $+      shouldNotTypecheck (cast d :: B)+    it "correctly fails to cast D to C" $+      shouldNotTypecheck (cast d :: C)+    it "correctly fails to cast E to B" $+      shouldNotTypecheck (cast e :: B)+    it "correctly fails to cast E to C" $+      shouldNotTypecheck (cast e :: C)+    -- The following two produce type errors as expected.+    -- Unfortunately, user-defined type errors in combination+    -- with shouldNotTypeCheck seems to trigger an internal+    -- error ... (see GHC bug #12104)+{-+    it "fails to cast F to anything (even X)" $+      shouldNotTypecheck (cast f :: X)+    it "fails to cast G to anything (even X)" $+      shouldNotTypecheck (cast g :: X)+-}