[Proposal] Renaming (:=:) to (==)

[Edward Kmett]

On Sat, Oct 12, 2013 at 1:29 AM, Iavor Diatchki <iavor.diatchki at gmail.com>wrote:

> Hello,
>
> I am not sure what version of GHC.TypeLits you looked at, but as of the
> other day the code in there is almost the same as what you propose (except
> for the use of different classes).
>

My copy of the code was a couple of days out of date, from when I started
the patch.

On Fri, Oct 11, 2013 at 12:54 PM, Edward Kmett <ekmett at gmail.com> wrote:
>
>>
>> They are currently impossible to implement without using very deep
>> voodoo. See the magicSingIId note.
>>
>>
> The `magicSingI` has been redone and is quite a bit simpler now.  Note
> [magicDictId magic] describes the current approach. Still, if we can think
> of a way to get rid of it, I'm strongly in support.
>
>
>> If we bring in GHC.Reflection. (I've almost finished a patch for it, my
>> only remaining hangups are in the wiredIn itself) then the code in
>> GHC.TypeLits for KnownNat and KnownSymbol can go away, and those two
>> definitions can use reflection internally.
>>
>>

> `KnowNat` and `KnownSymbol` are the basic classes that provide the
> built-in instances for type-level literals (SingI is gone).  I don't see
> any way around having some built-in code like that.
>

Indeend, `natVal` is implemented almost exactly like this.  It'd be trivial
> to provide an instance for the `Reify` class if we needed to:
>
>   instance KnowNat n => Reifying (n :: Nat) where type Reified n =
> Integer; reflect# = natVal
>
> If those are the classes being generated now, then I can use that to
generate the instances for Reifying at those kinds.

>

> Those classes can melt away and disappear
>>
>>
> Do you mean by providing built-in instances for `Reify` instead? If so,
> this is mostly a renaming, and I am not so keen on making the change as I
> like the simplicity of `KnownSym` and `KnownNat`.  Also---and this is an
> implementation detail---their dictionaries are simpler than the one for
> `Reify`: they just carry around the actual value, integer or string, while
> the dictionaries for `Reify` have to store a whole function.  I think this
> matters when you package them in existentials, no?
>

The instance for Reifying holds a function from Proxy# a which is of
unlifted kind and has no representation. Behind the scenes they should look
substantially identical.

Using something like the Tagged newtype could make them definitely
identical behind the scenes.

I'm okay with leaving them as it is. I mostly was noting that if we did
consolidate then we'd get a slight code reduction.


>  and internally the implementation of someNatVal, and someSymbolValbecome much less horrific:
>>
>> -- | This type represents unknown type-level natural numbers.
>> data SomeNat    = forall (n :: Nat).    Reifying n => SomeNat    (Proxy# n)
>>
>> -- | Convert an integer into an unknown type-level natural.
>> someNatVal :: Integer -> Maybe SomeNat
>> someNatVal n
>>   | n >= 0    = Just (reify# n SomeNat)
>>   | otherwise = Nothing
>>
>>
> Well, the current implementation is almost exactly this! I don't really
> know how `reify#` is supposed to work, but it certainly seems to do
> something very similar to what `magicDict` does, so we should probably make
> sure that there is only one implementation.  I would guess that you can use
> `magicDict` to implement `reify#`.  The other way around would also be OK
> with me as long as I don't have to use the `Reify` class, and can use
> directly the simpler (no type functions, no kind polymorphism)
> `KnownSymbol` and `KnownNat` classes.
>

In core, stripping away the newtypes and coercions reify# winds up looking
like

reify a k = k (\_ -> a) proxy#

The lambda there is ignoring a Proxy#, which is an unlifted argument
without representation, and the proxy# argument at the end is similar.

Also, doesn't `reify#` introduce a coherence issue?  `someNatVal` and the
> instances for `KnownNat` are carefully engineered to provide a consistent
> view to the programmer, but as far as understand, this is not the case with
> `Reifying`.  For example, consider the following code:
>

data {- kind -} K
>
> instance Reifying (a :: K) where
>   type Reified a = Integer
>   reflect# _ = 5
>
> getK :: Reifying a => Proxy (a :: K) -> Integer
> getK = reflect#
>
> test :: Integer
> test = reify# 6 getK
>
> It is not at all obvious if `test` should evaluate 5 (using the global
> instance) or 6 (using the locally supplied evidence), and the choice seems
> highly dependent on the mood of the constraint solver.
>

Fair point. I was attempting to generalize reify# to allow it to
instantiate at kinds other than *, to enable it to subsume your existing
usecase.

When restricted to * there isn't a coherence issue, as there is no such
overarching instance, but also simply by providing any concrete instance of
Reifying under kind * means that any attempt by the user to define
such an instance
Reifying (a :: *) would overlap, preventing this conflict.

I'll go back to the simpler version of reify#, which doesn't attempt to let
you reify at other kinds, and leave TypeLits alone.

This simplifies my task considerably.

-Edward
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20131012/0424e4e8/attachment.html>