{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# 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