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

Move ccase_SList into All class #149

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

ryantrinkle
Copy link

This allows us to provide more type information to the continuations.

Specifically: cpara_SList doesn't allow the cons continuation to know that there's a connection between (y ': ys) and xs. With this change, ccase_SList does provide that connection, i.e. that (y ': ys) ~ xs.

I'm not sure whether this is a breaking change or not: it should provide strictly more info to the continuations, and I don't think it's sensible for anyone to be defining their own instances of All.

This allows us to provide more type information to the continuations
@kosmikus
Copy link
Member

kosmikus commented Jan 2, 2022

Thanks for the PR, @ryantrinkle . I'm currently still a bit reluctant to just merge, because I'd like to understand the underlying issue. To me, cpara_SList is one of the most general functions there are and if ccase_SList after your change can no longer be expressed in terms of cpara_SList, then I'd think that cpara_SList should be changed. Also, is it possible for you to give an example of a definition that requires this change?

@kosmikus
Copy link
Member

kosmikus commented Jan 3, 2022

Ok, I don't think ccase_SList has to be moved into the class, as I think it can be expressed in terms of cpara_SList as follows:

newtype CCase xs r ys = MkCCase { unCCase :: (xs ~ ys) => r ys }

ccase_SList ::
     All c xs
  => proxy c
  -> ((xs ~ '[]) => r '[])
  -> (forall y ys . (xs ~ (y : ys), c y, All c ys) => r (y ': ys))
  -> r xs
ccase_SList p nil cons =
  unCCase (cpara_SList p (MkCCase nil) (const (MkCCase cons)))
{-# INLINE ccase_SList #-}

I would furthermore think that it's then even sufficient to change the type of ccase_SList to

ccase_SList ::
     All c xs
  => proxy c
  -> ((xs ~ '[]) => r '[])
  -> (forall y ys . (xs ~ (y : ys)) => r (y ': ys))
  -> r xs

@kosmikus kosmikus added this to the 0.6 milestone Jan 8, 2022
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

Successfully merging this pull request may close these issues.

2 participants