I think I’m starting to get the hang of GHC.Generics. @ashokkimmel ‘s example was a great primer for getting me used to looking at how type families and perform type-level computation.
A few weeks later and a lot more manual head-smashing against wall and Hackage Docs and I think I have something now that I can be relatively proud of and I’m happy with as learning resource.
The main hangup was getting a working GFromBitStructure (S1 m (Rec0 (Field name width))) instance, it was difficult for me to prove that the width in the Field was the same as the one provided by the pattern matched Field value constructor. This was mainly due to the previous approach using a type family to keep track of the position in the BitStructure fs by recursively fetching the remainder of the list. After creating the ToList type family however, that got rid of that problem but then introduced a new problem with the GFromBitStructure (a :*: b) which now needed an unsafeCoerce to solve.
Perhaps more type work has to be done to avoid using it but it works and I go backwards and forwards between standard ADT representations and the rest of the machinery.
This is Materials.Properties.Generic.Types
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Materials.Properties.Generic.Types where
import Data.Kind (Type)
import GHC.Generics
import GHC.TypeLits
import Materials.Properties.Types
import Unsafe.Coerce (unsafeCoerce)
type family Append (xs :: [k]) (ys :: [k]) :: [k] where
Append '[] ys = ys
Append (x ': xs) ys = x : Append xs ys
-- | Unfortunately takes converts to and from generic representation of BitStructure
-- rather than handwritten BitStructure
class HasBitStructureRep a where
toStruct :: a -> BitStructure (GLayout (Rep a))
fromStruct :: BitStructure (GLayout (Rep a)) -> a
-- | Class for making BitStructures generically
class GToBitStructure f where
type GLayout f :: [Type]
gToStruct :: f a -> BitStructure (GLayout f)
instance GToBitStructure U1 where
type GLayout U1 = '[]
gToStruct U1 = End
-- | Combines intermediate generic structures together.
instance (GToBitStructure a, GToBitStructure b) => GToBitStructure (a :*: b) where
type GLayout (a :*: b) = GLayout a `Append` GLayout b
gToStruct (a :*: b) = gToStruct a `appendStructure` gToStruct b
where
appendStructure :: BitStructure as -> BitStructure bs -> BitStructure (as `Append` bs)
appendStructure End ys = ys
appendStructure (x :&: xs) ys = x :&: appendStructure xs ys
instance (GToBitStructure f) => GToBitStructure (D1 m f) where
type GLayout (D1 m f) = GLayout f
gToStruct (M1 x) = gToStruct x
instance (GToBitStructure f) => GToBitStructure (C1 m f) where
type GLayout (C1 m f) = GLayout f
gToStruct (M1 x) = gToStruct x
-- | If we have a record selector that points to a Field name w, add it to our list
instance (KnownNat w) => GToBitStructure (S1 m (Rec0 (Field name w))) where
type GLayout (S1 m (Rec0 (Field name w))) = '[Field name w]
gToStruct (M1 (K1 f)) = f :&: End
-- | Generates type level lists from the generic types of interest.
type family ToList (f :: k -> Type) :: [Type] where
ToList (M1 i c f) = ToList f
ToList (f :*: g) = ToList f `Append` ToList g
ToList (K1 i v) = '[v]
-- | When going from a BitStructure, find the first element and convert it into a Rep
-- and also return the remaining structure to recursively walk through
class GFromBitStructure f where
gFromStruct :: BitStructure (ToList f `Append` rest) -> (f p, BitStructure rest)
instance (GFromBitStructure f) => GFromBitStructure (D1 m f) where
gFromStruct fs =
let (x, rest) = gFromStruct fs
in (M1 x, rest)
instance (GFromBitStructure f) => GFromBitStructure (C1 m f) where
gFromStruct fs =
let (x, rest) = gFromStruct fs
in (M1 x, rest)
-- | Since we're only dealing with the first element, we can be assured that the w
-- here is the same as what we later assign
instance (KnownU w) => GFromBitStructure (S1 m (Rec0 (Field name w))) where
gFromStruct (Field w :&: rest) = (M1 (K1 (Field @name @w w)), rest)
-- | Couldn't acheive this any other way; after learning about unsafeCoerce it seemed the most sensible way
-- reducing the type level lists inferred by GHC would have returned the same result.
-- Will certainly not make it a habit
instance (GFromBitStructure a, GFromBitStructure b) => GFromBitStructure (a :*: b) where
gFromStruct fs =
let (l, mid) = gFromStruct @a (unsafeCoerce fs)
(r, end) = gFromStruct @b mid
in (l :*: r, end)
newtype GenericBitStructure a = GenericBitStructure a
deriving newtype instance (Generic a) => Generic (GenericBitStructure a)
instance (Generic a, GFromBitStructure (Rep a), GToBitStructure (Rep a)) => HasBitStructureRep (GenericBitStructure a) where
toStruct = defaultToStruct
fromStruct = defaultFromStruct
defaultToStruct :: (GToBitStructure (Rep a), Generic a) => a -> BitStructure (GLayout (Rep a))
defaultToStruct = gToStruct . from
-- | The type applications here represent the two type-level arguments that get passed to `Append`.
-- Since we append the BitStructure (Rep a) layout appended to empty list, it is functionally the same as
-- just having the BitStructure (Rep a) list.
-- unsafeCoerce is to prove to the type checker that (ToList (Rep a) `Append` '[]) is the same as GLayout (Rep a)
defaultFromStruct :: forall a. (GFromBitStructure (Rep a), Generic a) => BitStructure (GLayout (Rep a)) -> a
defaultFromStruct structure =
let (rep, _) = gFromStruct @(Rep a) @'[] (unsafeCoerce structure)
in to rep
data R11G11B10 = R11G11B10
{ r :: Field 'R 11,
g :: Field 'G 11,
b :: Field 'B 10
}
deriving (Generic, Show)
deriving HasBitStructureRep via GenericBitStructure R11G11B10
-- >>> testPixel
-- 255 :&: (2052 :&: (124 :&: End))
-- >>> unpack $ pack testPixel
-- 255 :&: (4 :&: (124 :&: End))
testPixel :: BitStructure [Field 'R 11, Field G 11, Field B 10]
testPixel = toStruct $ R11G11B10 255 2052 124
-- >>> testConversion
-- R11G11B10 {r = 255, g = 4, b = 124}
testConversion :: R11G11B10
testConversion = fromStruct . unpack . pack $ testPixel
-- >>> testConversion2
-- 255 :&: (4 :&: (124 :&: End))
testConversion2 = toStruct . fromStruct @R11G11B10 . unpack . pack $ testPixel
A lot learned and it’s still quite hairy and scary stuff but I’m happy with the progress.
The API itself does leave a lot of holes and question marks: for example, I don’t believe I have any way of constraining Channels only being used once and frankly, it’s more work than I willing to put in to make that illegal.
On the plus side, I’m much more confident with things that involve type-level programming than I was before I started this so I do think it has been a worthwhile time-spend.