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

[Iavor Diatchki]

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).

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.




> Then the current instances for KnownNat and KnownSymbol become the
> substantially identical actual instances we currently have for them in the
> reflection package:
>
> -- | This instance gives the integer associated with a type-level natural.
> -- There are instances for every concrete literal: 0, 1, 2, etc.
> instance SingI n => Reifying (n :: Nat) where
>   type Reified n = Integer
>   reflect# _ = case sing :: Sing n of
>     SNat x -> x
>
>
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


> 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?




> and internally the implementation of someNatVal, and someSymbolVal become
> 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.

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.

-Iavor
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20131011/c59649ef/attachment.html>