Plutonomicon / plutarch-core

Plutarch 2.0
MIT License
19 stars 6 forks source link

Simplified generics implementation #18

Closed AriFordsham closed 1 year ago

AriFordsham commented 1 year ago

The main advantage, besides simplified implementation, Is that the Plutarch-side code [[PType]] is exposed via the constraint IsPCodeOf, rather than being an existential quantification, vastly improving ergonomics.

L-as commented 1 year ago

Using hcoerce is a minor upgrade, but actually, it seems it's also implemented under the hood with unsafeCoerce... Less unsafeCoerce is still better, but right now we don't use any unsafeCoerce.

AriFordsham commented 1 year ago

hcoerce narrows the unsafety surface of coercion by using a specialization expected to be safe. This could be implemented fully safely, at the cost of (compile-time) performance.

re-xyr commented 1 year ago

I experimented a little and got a version with associated type families to work:

class
  ( SOP.AllZip (SOP.LiftedCoercible SOP.I (Term edsl)) ts (PPPTypes ts)
  , SOP.AllZip (SOP.LiftedCoercible (Term edsl) SOP.I) (PPPTypes ts) ts
  , SOP.All (IsPType edsl) (PPPTypes ts)
  ) =>
  PIsProduct (edsl :: PDSLKind) (ts :: [Type])
  where
  type PPPTypes ts :: [PType]
instance PIsProduct edsl '[] where
  type PPPTypes '[] = '[]
instance (IsPType edsl a, PIsProduct edsl ts) => PIsProduct edsl (Term edsl a : ts) where
  type PPPTypes (Term edsl a : ts) = a : PPPTypes ts

class
  ( SOP.AllZip2 (SOP.LiftedCoercible SOP.I (Term edsl)) tss (PSPTypes tss)
  , SOP.AllZip2 (SOP.LiftedCoercible (Term edsl) SOP.I) (PSPTypes tss) tss
  , SOP.SameShapeAs tss (PSPTypes tss)
  , SOP.SameShapeAs (PSPTypes tss) tss
  , SOP.AllZipF (SOP.AllZip (SOP.LiftedCoercible (Term edsl) SOP.I)) (PSPTypes tss) tss
  , SOP.AllZipF (SOP.AllZip (SOP.LiftedCoercible SOP.I (Term edsl))) tss (PSPTypes tss)
  , SOP.All2 (IsPType edsl) (PSPTypes tss)
  , SOP.SListI2 tss
  ) =>
  PIsSum (edsl :: PDSLKind) (tss :: [[Type]])
  where
  type PSPTypes (tss :: [[Type]]) :: [[PType]]
instance PIsSum edsl '[] where
  type PSPTypes '[] = '[]
instance (PIsProduct edsl ts, PIsSum edsl tss) => PIsSum edsl (ts : tss) where
  type PSPTypes (ts : tss) = PPPTypes ts : PSPTypes tss

type PSOPTerms edsl a = SOPG.GCode (PConcrete edsl a)
type PSOPPTypes edsl a = PSPTypes (PSOPTerms edsl a)

class
  ( PGeneric a
  , PIsSum edsl (PSOPTerms edsl a)
  , PReprSort a ~ PReprSOP
  ) =>
  PIsSOP (edsl :: PDSLKind) (a :: PType)
instance
  ( PGeneric a
  , PIsSum edsl (PSOPTerms edsl a)
  , PReprSort a ~ PReprSOP
  ) =>
  PIsSOP (edsl :: PDSLKind) (a :: PType)

sopFrom ::
  forall edsl a.
  PIsSOP edsl a =>
  Proxy edsl ->
  Proxy a ->
  SOP.SOP SOP.I (PSOPTerms edsl a) ->
  SOP.SOP (Term edsl) (PSOPPTypes edsl a)
sopFrom _ _ = SOP.hcoerce

sopTo ::
  forall edsl a.
  PIsSOP edsl a =>
  Proxy edsl ->
  Proxy a ->
  SOP.SOP (Term edsl) (PSOPPTypes edsl a) ->
  SOP.SOP SOP.I (PSOPTerms edsl a)
sopTo _ _ = SOP.hcoerce

specifically the "inner" types still don't leak to the class signature, which is nice.

AriFordsham commented 1 year ago

I see 'leaking' the signature as a feature, not a bug - those types are useful and not particulary private.

@re-xyr Would you mind to submit that as a PR against this branch so I can look at it properly?

re-xyr commented 1 year ago

I opened a PR. I don't really mind leaking the signatures or not, because I can't think of any significant downside to either. @L-as what do you think?

AriFordsham commented 1 year ago

Oh, I thought you got fundeps working. I specifically wrote this change in order to expose the inner types.

re-xyr commented 1 year ago

Well, I guess I'll try to make fundeps work tomorrow...

AriFordsham commented 1 year ago

I got as far as getting lost trying to define a pile of injective type families.

L-as commented 1 year ago

This is an improvement.