Changes between Version 6 and Version 7 of TypeLevelReasoning

Feb 12, 2013 2:45:11 AM (5 years ago)



  • TypeLevelReasoning

    v6 v7  
    6767Gabor: I have created a new branch `type-reasoning` and pushed everything I have so far to the `libraries/base` repo. [ Richard's mail] summarizes what still needs to be done.
     69Richard (11 Feb 2013): I've just pushed a commit to the type-reasoning branch with a strawman proposal of a reorganization of these definitions. Specifically, this commit breaks !TypeLits into the following five files:
     71 - GHC.!TypeEq, which contains the definitions for (:~:), Void, Refuted, etc.
     72 - GHC.Singletons, which contains the definitions about singletons in general, such as SingI and !SingEquality
     73 - GHC.!TypeLits.Unsafe, which contains just unsafeSingNat and unsafeSingSymbol
     74 - GHC.!TypeLits.Internals, which is necessary to get GHC.!TypeLits.Unsafe to have access to the right internals; this module is not exported from the 'base' package
     75 - GHC.!TypeLits, which contains the definitions specific to type-level literals.
     77Some thoughts on this design:
     78 - First off, why is !TypeEq part of GHC?? Because we wish to write eqSingNat and eqSingSym in GHC.!TypeLits, and that module rightly deserves to be part of GHC. I'm quite uncomfortable with this decision, and I even created a new git repo at [] to hold the definitions that eventually ended up in GHC.!TypeEq. (The repo has nothing in it, now.) Perhaps the best resolution is to move eqSingNat and eqSingSym out of GHC.!TypeLits and into an external package, but that seems silly in a different direction. (It is fully technically feasible, as those functions don't depend on any internals.) I would love some feedback here.
     79 - Why is Singletons broken off? No strong reason here, but it seemed that the singletons-oriented definitions weren't solely related to type-level literals, so it seemed more natural this way.
     80 - Making the Unsafe module was a little more principled, because those functions really are unsafe! They are quite useful, though, and should be available somewhere.
     81 - Currently, the internals of GHC assign types like "0" the kind GHC.!TypeLits.Nat, so Nat and Symbol '''must''' remain in the GHC.!TypeLits module. Unfortunately, the plumbing around GHC.!TypeLits.Unsafe want Nat and Symbol to be defined in GHC.!TypeLits.Internals. So, I created a !TypeLits.hs-boot file to fix the problem. This is highly unsatisfactory, and if something like what I've done here sticks around, we should change the internals of GHC to use GHC.!TypeLits.Internals.Nat, getting rid of the import cycle.
     82 - I've put in the decideSing function as discussed further up in this thread. Its implementation for Nat and Symbol must use unsafeCoerce, but that shouldn't be a surprise.
     84Unfortunately, the code doesn't compile now. This is because it needs SingI instances for, say, Sing 0. For a reason I have not explored, these instances are not available here, though they seem to be for code written outside of GHC. Iavor, any thoughts on this?
     86Please tear any of these ideas (or my whole commit) to shreds! It really is meant to be a strawman proposal, but committing these changes seemed the best way of communicating on possible set of design decisions.