Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Partial type constructors #5

Open
9 of 10 tasks
jgbm opened this issue Dec 23, 2021 · 1 comment
Open
9 of 10 tasks

Partial type constructors #5

jgbm opened this issue Dec 23, 2021 · 1 comment
Assignees

Comments

@jgbm
Copy link
Contributor

jgbm commented Dec 23, 2021

This issue is to track the different work needed to support partial type constructors.

Core features

Low-level libraries and language features

  • Worker-wrapper transformations
  • Rules
  • Deriving
  • Generics
  • Total and its kin (following Richard's cheat)
@jgbm jgbm self-assigned this Dec 23, 2021
fxdpntthm added a commit that referenced this issue Apr 14, 2022
  - The idea is to treat them as data types and not type syn fam
  - Reason to do so is that they can have variable arity
  - do not generate `wf'DF` name for a `DF` type family.
  - we instead generate `DF @ a ~ ()` etc.
- some updates to haskeline
- `GHC.Generics.Generically` typeclass instances uncommented
- Change the names of the type family axioms
  - They now include the names of the type constructors
- Reduce the calls to unsafe `wfMirrorTyCon`
- Push the generation of wf family instances in a more appropriate place
  - Moved it into `tcTyFamInstDecl` instead of `tcInstDecls1`
@fxdpntthm
Copy link
Collaborator

fxdpntthm commented May 3, 2022

Rules that don't behave

GHC.Control.Category
class Category cat where
    -- | the identity morphism
    id :: cat a a

    -- | morphism composition
    (.) :: cat b c -> cat a b -> cat a c

{-# RULE
"association"   forall p q r .
                 (p . q) . r = p . (q . r)
 #-}

the association rule fails to compile as it gives rise to different constraints on each side of the equality.

GHC.Control.Arrow
class Category a => Arrow a where
....

{-# RULES
-- "compose/arr"   forall f g .
--                 (arr f) . (arr g) = arr (f . g)
"first/arr"     forall f .
                first (arr f) = arr (first f)
"second/arr"    forall f .
                second (arr f) = arr (second f)
"product/arr"   forall f g .
                arr f *** arr g = arr (f *** g)
"fanout/arr"    forall f g .
                arr f &&& arr g = arr (f &&& g)
-- "compose/first" forall f g .
--                 (first f) . (first g) = first (f . g)
-- "compose/second" forall f g .
--                 (second f) . (second g) = second (f . g)
 #-}


class Arrow a => ArrowChoice a where
...

{-# RULES
"compose/left"  forall f g .
                 left f . left g = left (f . g)
"compose/right" forall f g .
                 right f . right g = right (f . g)
 #-}

Update:

Don't actually need to comment out these after adding Total2 as a class constraint: 90d3c63
class Total2 cat => Category cat where, class (Total2 a, Arrow a) => ArrowChoice a etc.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants