darcs

Patch 1807 drop our custom EqCheck type for (:~:) from base

Title drop our custom EqCheck type for (:~:) from base
Superseder Nosy List ganesh
Related Issues
Status in-discussion Assigned To
Milestone

Created on 2019-06-09.12:03:38 by ganesh, last changed 2019-06-14.18:27:40 by bf.

Files
File name Status Uploaded Type Edit Remove
drop-our-custom-eqcheck-type-for-_____-from-base.dpatch ganesh, 2019-06-09.12:03:38 application/x-darcs-patch
drop-our-custom-eqcheck-type-for-_____-from-base.dpatch ganesh, 2019-06-11.07:11:57 application/x-darcs-patch
patch-preview.txt ganesh, 2019-06-09.12:03:38 text/x-darcs-patch
patch-preview.txt ganesh, 2019-06-11.07:11:57 text/x-darcs-patch
unnamed ganesh, 2019-06-09.12:03:38 text/plain
unnamed ganesh, 2019-06-11.07:11:57 text/plain
See mailing list archives for discussion on individual patches.
Messages
msg20704 (view) Author: ganesh Date: 2019-06-09.12:03:38
Just for discussion for now. I've replaced EqCheck wA wB
with Maybe (wA :~: wB).

It's always nice not to roll our own for standard concepts,
and it means we can occasionally use (wA :~: wB) directly.

On the other hand the change will probably conflict with
other WIP, and it does make things a bit more verbose -
e.g. Just Refl is longer than IsEq.

1 patch for repository darcs-unstable@darcs.net:screened:

patch 8a9b8365cb739b10bc1b282109da85a55e78c3a2
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Sun Jun  9 10:52:37 BST 2019
  * drop our custom EqCheck type for (:~:) from base
Attachments
msg20707 (view) Author: ganesh Date: 2019-06-11.07:11:57
Updated bundle with more possible updates to witnesses etc.

I'm not sure any of them except dropping Darcs.Patch.Type
is that compelling. The 'role nominal' one isn't very
invasive and adds a bit of safety, so is probably worth it
as well.

4 patches for repository darcs-unstable@darcs.net:screened:

patch 8a9b8365cb739b10bc1b282109da85a55e78c3a2
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Sun Jun  9 10:52:37 BST 2019
  * drop our custom EqCheck type for (:~:) from base

patch c1f343cadad9a2f1ba9fdaa1cc8fb1226d1cbc08
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Tue Jun 11 07:06:02 BST 2019
  * make sure patch context witnesses have role nominal
  
  This makes sure calling code can't use coerce to change the
  witnesses.
  
  We only need to do this for the low-level types. Higher-level
  ones that take other patches as parameters will have this role
  inferred anyway.

patch 34588de518a656932affad4fa33556612b8e47a7
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Tue Jun 11 07:37:58 BST 2019
  * Give patch contexts their own kind

patch 4b92c674ba371121fe71234b349a01989ba21e78
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Tue Jun 11 08:08:05 BST 2019
  * drop Darcs.Patch.Type and use TypeApplications instead
Attachments
msg20719 (view) Author: bf Date: 2019-06-11.16:58:03
> Just for discussion for now. I've replaced EqCheck wA wB
> with Maybe (wA :~: wB).
> 
> It's always nice not to roll our own for standard concepts,
> and it means we can occasionally use (wA :~: wB) directly.
> 
> On the other hand the change will probably conflict with
> other WIP, and it does make things a bit more verbose -
> e.g. Just Refl is longer than IsEq.

I like the idea though I haven't been looking at the changes in details
yet. Your comment about conflicts with WIP is appreciated, indeed I
would like you to postpone this until we get V3 in screened. I think I
need to make a bundle for that sooner rather than later.
msg20808 (view) Author: bf Date: 2019-06-14.18:27:40
> Updated bundle with more possible updates to witnesses etc.
> 
> I'm not sure any of them except dropping Darcs.Patch.Type
> is that compelling.

Yes, this one strikes me as a nice way to make use of type application.
I am also fine with using it in the test harness, instead of passing
undefined :: Whatever.

> The 'role nominal' one isn't very
> invasive and adds a bit of safety, so is probably worth it
> as well.

Agreed.

Darcs.Patch.Witnesses.Kind looks interesting but it could use a bit of
documentation. I don't quite grok what's going on there...

It is a bit unfortunate that this bundle has so many conflicts with
screened now. (Sorry about that.) I guess it makes sense to rebase your
patches and resend, makes it a bit easier to apply and the view in a
side-by-side diff. (For now I helped myself with a 'darcs rebase apply'
in a separate clone.)
History
Date User Action Args
2019-06-09 12:03:38ganeshcreate
2019-06-09 12:05:21ganeshsetstatus: needs-screening -> in-discussion
2019-06-11 07:11:57ganeshsetfiles: + patch-preview.txt, drop-our-custom-eqcheck-type-for-_____-from-base.dpatch, unnamed
messages: + msg20707
2019-06-11 16:58:03bfsetmessages: + msg20719
2019-06-14 18:27:40bfsetmessages: + msg20808