RFC: Singleton equality witnesses

[Gabor Greif]

On 2/6/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>
> On Feb 6, 2013, at 1:03 PM, Gabor Greif wrote:
>
>> On 2/5/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>>
>>>
>>> My argument would be not to return
>>>  Maybe (SameSing kparam a b)
>>> but to return
>>>  Either (SameSing kparam a b) (SameSing kparam a b -> Void)
>>> or something similar. (Void is taken from the void package, but it could
>>
>> I see where you want to get at and recognize the added value. I have
>> two thoughts to add, though.
>>
>>  o most people are comfortable with assembling equality evidence (for
>> example by means of the Maybe monad), but few have done this for its
>> refutations.
>>
>>  o sometimes an equality proof is just what you need to proceed,
>> which is probably a smaller data structure to be created (laziness may
>> help here, but still allocates).
>
> I agree with these points, and I would want a function that returns Maybe …
> to be available. Essentially, I want what you've written -- a general
> "decide" function with a "semi-decide" wrapper. Programmers can choose not
> to implement the "decide" function if they don't want/need to.

Yeah, it is a bit dodgy to say "decideSing = undefined", but it may
become just easy to write the proof down.

>
>>
>> I also flipped the type arguments to Either, since 'Right' sounds like
>> "Yep" and should signify positive evidence. I believe the ErrorT monad
>> transformer also uses this convention.
>
> Wholeheartedly agreed.

Cool.

>
>>>
>>> Also, why generalize the return type with SameSing? Do you have a case
>>> where
>>> you would want the equality witness type to be other than (:~:)?
>>
>> This leaves open the possibility of non-constructivistic evidence (is
>> there such a thing?). For example I could imagine an infinite Nat-like
>> type (with different representation) where we have a refutation proof
>> that n < m-1 and a refutation of n > m+1, and this would allow us to
>> construct evidence for n=m. I have seen
>> http://queuea9.wordpress.com/2012/11/05/canonize-this/ (and more
>> recent ones).
>>
>
> This I'm not so sure of. I think that the evidence returned by sameSing
> needs to be isomorphic to (a ~ b) in some way for sameSing to be useful.
> While I can imagine more elaborate structures than (:~:) that can be reduced
> to (~), those structures then could also be reduced to (:~:). So, I think
> the generality remains even if you remove the associated type.
>

Okay, I have created a branch "type-reasoning" and pushed it to
darcs.haskell.org, just try to fill in the missing stuff and feel free
to create the other modules. I'll remove the

   type SameSing kparam :: k -> k -> *

from the class by tomorrow if you haven't done it yet.

>>>
>>> I've thrown together a wiki page at
>>> http://hackage.haskell.org/trac/ghc/wiki/TypeLevelReasoning with Gabor's
>>> code, my code, and some of my thoughts. Please add your thoughts and any
>>> ideas into the mix!
>>
>> I have commented on PropNot, suggesting alternatives.
>>
> +1 for Refuted.

Great, no change here.

>
> To define decideSing for Nat and Symbol, I think we would need to refine
> eqSingNat and eqSingSymbol to become decideSingNat and decideSingSymbol,
> using unsafeCoerce for both branches. If Nat and Symbol were real inductive
> kinds under the hood, the unsafeCoerce would be unnecessary; it is
> essentially an optimization here.
>
> The only thing that stops me from saying "push" is that I think there is a
> better organization for all of this. The ideas we're discussing here (things
> like the Void type) don't seem to belong in TypeLits -- it has nothing to do
> with literals. Time for a GHC.TypeReasoning module? Does someone have a
> better name?

Sounds okay. We can wiggle around on the new branch 'till we feel
comfortable, but I'd like to land this on master before the v7.8 train
leaves the station (i.e. the release branch is created).

Cheers,

    Gabor

>
> Richard