`generics-sop`: constructing sum

I don't really understand the Injection type, but I should.

2022-01-22 15:31:22

I was constructing sums by doing manual plumbing, which I suspect is the result of not understanding the above,

class MkSum (before :: [[PType]]) (x :: [PType]) (xs :: [[PType]]) where
  mkSum' :: NP (Term s) x -> NS (NP (Term s)) (Append before (x ': xs))

instance MkSum '[] x xs where
  mkSum' = Z

instance MkSum bs x xs => MkSum (b ': bs) x xs where
  mkSum' = S . mkSum' @bs @x @xs

type family Append (a :: [as]) (b :: [as]) :: [as] where
  Append '[] b = b
  Append (a ': as) b = a ': Append as b

Sridhar Ratnakumar

2022-01-22 16:28:46

I'm loving https://github.com/kosmikus/SSGEP/blob/master/LectureNotes.pdf so far, because there is a natural progression to understanding the seemingly gnarly things in generics-sop Hackage.

Sridhar Ratnakumar

2022-01-22 18:15:54

Page 35, sList :: SList xss is probably relevant, but ... going with the MkSum to begin with, and to get it all to compile. The above code is also buggy, so I had to manually derive instances for now,

-- | TODO: Use the injections from `generics-sop`.
 class MkSum (before :: [[Type]]) (x :: [Type]) (xs :: [[Type]]) where
   mkSum' :: NP I x -> NS (NP I) (Append (Reverse before) (x ': xs))

 instance MkSum '[] x xs where
   mkSum' = Z

 instance MkSum '[p1] x xs where
   mkSum' = S . Z

 instance MkSum '[p1, p2] x xs where
   mkSum' = S . S . Z
 instance MkSum '[p1, p2, p3] x xs where
   mkSum' = S . S . S . Z
 instance MkSum '[p1, p2, p3, p4] x xs where
   mkSum' = S . S . S . S . Z

 instance MkSum '[p1, p2, p3, p4, p5] x xs where
   mkSum' = S . S . S . S . S . Z

 instance MkSum '[p1, p2, p3, p4, p5, p7] x xs where
   mkSum' = S . S . S . S . S . S . Z

https://github.com/Plutonomicon/plutarch/commit/a6343c99ba11390cc9dfa9c73c600a9d04cdf08c

Sridhar Ratnakumar

2022-01-22 20:51:06

will aggregate these eventually to https://ladder.haskell.page/5/Generic

Sridhar Ratnakumar

2022-01-23 16:20:31

https://stackoverflow.com/questions/70824108/creating-a-sum-type-using-generics-sop

Sridhar Ratnakumar

2022-01-23 18:13:59

This makes MkSum generic, but I'm still not happy. Looks too complex,

class MkSum idx xss where
  mkSum :: NP I (TypeAt idx xss) -> NS (NP I) xss

instance MkSum 'FZ (xs ': xss) where
  mkSum = Z
instance MkSum idx xss => MkSum ('FS idx) (xs ': xss) where
  mkSum v = S $ mkSum @idx @xss v

type family Length xss :: N.Nat where
  Length '[] = 'N.Z
  Length (x ': xs) = 'N.S (Length xs)

class Tail' (idx :: Fin n) (xss :: [[k]]) where
  type Tail idx xss :: [[k]]

instance Tail' 'FZ xss where
  type Tail 'FZ xss = xss

instance Tail' idx xs => Tail' ('FS idx) (x ': xs) where
  type Tail ('FS idx) (x ': xs) = Tail idx xs
instance Tail' idx xs => Tail' ('FS idx) '[] where
  type Tail ('FS idx) '[] = TypeError ('Text "Tail: index out of bounds")

class  TypeAt' (idx :: Fin n) (xs :: [[k]]) where
  type TypeAt idx xs :: [k]

instance TypeAt' 'FZ (x ': xs) where
  type TypeAt 'FZ (x ': xs) = x

instance TypeAt' ('FS idx) (x ': xs) where
  type TypeAt ('FS idx) (x ': xs) = TypeAt idx xs

Sridhar Ratnakumar

2022-01-24 16:52:20

Looks like this is not possible, but hey - that StackOverflow answer (which looks to be wrong) had me use Nat from base:

class MkSum (idx :: Nat) (xss :: [[Type]]) where
  mkSum :: NP I (IndexList idx xss) -> NS (NP I) xss

instance {-# OVERLAPPING #-} MkSum 0 (xs ': xss) where
  mkSum = Z
instance {-# OVERLAPPABLE #-}
  ( MkSum (idx-1) xss
  , IndexList idx (xs ': xss) ~ IndexList (idx-1) xss
  ) => MkSum idx (xs ': xss) where
  mkSum x = S $ mkSum @(idx-1) @xss x

This code is used here: https://twitter.com/sridca/status/1485656368635912198

Niiiice https://twitter.com/sridca/status/1485656368635912198/photo/1

- slow (@sridca)

`generics-sop`: constructing sum - Hacker Log