fumieval / extensible

Extensible records, variants, structs, effects, tangles
BSD 3-Clause "New" or "Revised" License
128 stars 20 forks source link

Why not defined type family `(++)` of Record and Variant #17

Closed matsubara0507 closed 5 years ago

matsubara0507 commented 6 years ago

type family (++) of type lebel list is defined in extensible.

But, undefined (++) for Record and Variant. if defined one, We can write below code:

type A = Record '[ "aaa" >: Bool ]
type B = A ++ Record '[ "bbb" >: Bool ]

Of course, We can define A andB after defining the type of fields type FieldA = '["aaa">: Bool] without one. But, I think that it's more useful if (++) for Record is defined.

I think that it's easy to define using PolyKInds.

type family (++) (t1 :: a) (t2 :: a) :: a where
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': xs ++ ys
  (h :* xs) ++ (h :* ys) = h :* (xs ++ ys)
  (h :| xs) ++ (h :| ys) = h :| (xs ++ ys)

Can I create a PR ?

fumieval commented 6 years ago

I don't think so. (++) should be well-kinded. Still you can create such a type family with a different name.