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

Fri Oct 11 20:12:43 UTC 2013

Dan just asked me what unsafeCoerce# was doing in the GHC.Reflection
imports above. unsafeCoerce# was only imported there while I was testing
this as a base only change to make sure I had the API right before I
started switching over to the wiredIn.

That won't be there in the final product.

-Edward

On Fri, Oct 11, 2013 at 3:54 PM, Edward Kmett <ekmett at gmail.com> wrote:

> On Fri, Oct 11, 2013 at 3:03 PM, Richard Eisenberg <eir at cis.upenn.edu>
>  wrote:
>
> I've done this (summarizing the issues discussed in this thread) and
>> posted at
>> http://ghc.haskell.org/trac/ghc/wiki/TypeLevelNamingIssues
>>
>> The color on the bikeshed may only be cosmetic, but we (and others) will
>> be looking at it for a long time. And, besides, I imagine many Haskellers
>> are aesthetes at heart. What else drew us to such a beautiful language? :)
>>
>>
> Thoughts on my first reading:
>
> Re Sym in Data.Type.Coercion:
>
> Sym shouldn't be (and at last check wasn't) exported by Data.Type.Coercion
> .
> It is only used to implement
>
> sym :: Coercion a b -> Coercion b a
>
> internally. It does so by using the supplied Coercion to coerce Sym a ainto Sym
> a b and unwrapping it to get Coercion b a.
>
> This is an adaptation of the pretty standard standard trick for
> implementing sym with Leibnizian equality.
>
> Similarly `trans` / (.) are implementing by using coerce on a Coercion,
> since its arguments are representational.
>
> This lets us get away with using Coercible directly as it stands, and
> still gives us the right groupoid structure for the witness.
>
>
> Simon's suggestion of castWith sounds fine to me, and is much nicer than
> subst.
>
> Re: The need for SomeNat and SomeSymbol
>
> They are currently impossible to implement without using very deep voodoo.
> See the magicSingIId note.
>
> 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.
>
> We'd pick up
>
> module GHC.Reflection
>
>   ( Reifying(..)
>
>
>   , reify#
>
>   ) where
>
>
> import GHC.Prim (Proxy#, proxy#, unsafeCoerce#)
>
>
> class Reifying s where
>
>   type Reified s :: *
>
>
>   -- | Recover a reified value.
>
>   reflect# :: Proxy# s -> Reified s
>
>
>
> -- wiredIn
>
> reify# :: forall k a r. a -> (forall (s :: k). (Reifying s, Reified s ~ a) => Proxy# s -> r) -> r
>
>
> 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
>
> -- | This instance gives the string associated with a type-level symbol.
> -- There are instances for every concrete literal: "hello", etc.
> instance SingI n => Reifying (n :: Symbol) where
>   type Reified (n :: Symbol) = String
>   reflect# _ = case sing :: Sing n of
>     SSym x -> x
>
>
> Those classes can melt away and disappear 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)
>
> -- | This type represents unknown type-level symbols.
> data SomeSymbol = forall (n :: Symbol). Reifying n => SomeSymbol (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
>
> -- | Convert a string into an unknown type-level symbol.
> someSymbolVal :: String -> SomeSymbol
> someSymbolVal n = reify# n SomeSymbol
>
>
> The combinators then can just use reflect#.
>
>
> instance Eq SomeNat where
>
>   SomeNat x == SomeNat y = reflect# x == reflect# y
>
>
> instance Ord SomeNat where
>
>   compare (SomeNat x) (SomeNat y) = compare (reflect# x) (reflect# y)
>
>
> instance Show SomeNat where
>
>   showsPrec p (SomeNat x) = showsPrec p (reflect# x)
>
>
> This minimalist version of GHC.Reflection seems to actually result in a
> net reduction in the amount of code. It also makes both of those types
> candidates for moving out, as they don't rely on a terrifying builtin with
> a fake type.
>
>
> -Edward
>
> On Oct 3, 2013, at 4:10 AM, Simon Peyton-Jones wrote:
>>
>> I'm not aware of a wide poll on the names in TypeLits, so we shouldn't
>> necessarily just follow that lead. That said, the above proposal about `?`
>> seems sensible to me. If we decide to do this, we should find somewhere
>> (where??) to articulate this.****
>> ** **
>> Negotiating names is not much fun, but they stay with us for a long
>> time.  And Richard, might you find 20 mins to throw up a wiki page (on the
>> GHC Trac or Haskell wiki, doesn?t matter too much) giving the exported
>> signature of TypeLits and related modules (singletons?), together with a
>> summary of the main open naming issues?  Should be mainly cut-and-paste.
>> That would be really helpful.****
>> ** **
>> Simon****
>> ** **
>>  *From:* Libraries [mailto:libraries-bounces at haskell.org] *On Behalf Of *Richard
>> Eisenberg
>> *Sent:* 03 October 2013 04:07
>> *To:* Edward Kmett
>> *Cc:* Haskell Libraries
>> *Subject:* Re: [Proposal] Renaming (:=:) to (==)****
>> ** **
>> Thanks for pointing this out, Edward. I think consistency within the type
>> level is more important than consistency between the type level and the
>> term level. So, if we settle on a convention that a symbol ending in `?`
>> means Boolean-valued and other symbols mean constraints, I'm all for making
>> the change to (==).****
>> ** **
>> I'm not aware of a wide poll on the names in TypeLits, so we shouldn't
>> necessarily just follow that lead. That said, the above proposal about `?`
>> seems sensible to me. If we decide to do this, we should find somewhere
>> (where??) to articulate this.****
>> ** **
>> Richard ****
>> ** **
>> On Oct 2, 2013, at 9:28 PM, Edward Kmett <ekmett at gmail.com> wrote:****
>>
>>
>> ****
>>
>> GHC.TypeLits code looks to be using (<=?) as the boolean valued version
>> of the predicate and (<=) for the assertion.****
>> ** **
>> This points to a coming disagreement over style across the different
>> parts of GHC itself, if we're saying that the principle reason for not
>> using (==) is that we want it to be the boolean valued version.****
>> ** **
>> -Edward****
>>
>> ** **
>> On Mon, Sep 30, 2013 at 4:03 PM, Carter Schonwald <
>> carter.schonwald at gmail.com> wrote:****
>>
>> Agreed. ****
>>
>>
>> On Monday, September 30, 2013, Edward A Kmett wrote:****
>>
>> I think if someone went through the effort of writing a patch so you
>> could at least introduce local operator names with an explicit forall, like
>> with ScopedTypeVariables and the proposed explicit type applications then
>> it'd probably be accepted.
>>
>> Sent from my iPhone****
>>
>>
>> On Sep 30, 2013, at 2:25 PM, Conal Elliott <conal at conal.net> wrote:****
>>
>> -1.****
>>
>> I'm hoping we don't get more deeply invested in the syntactic change in
>> GHC 7.6 that removed the possibility of symbolic type variables ("~>", "*",
>> "+", etc). I had a new job and wasn't paying attention when SPJ polled the
>> community. From my perspective, the loss has much greater scope than the
>> gain for type level naturals. I'd like to keep the door open to the
>> possibility of bringing back the old notation with the help of a language
>> pragma. It would take a few of us to draft a proposal addressing details.
>> ****
>>
>> Not at all meaning to start a syntax debate on this thread. Just an
>> explanation of my -1 for the topic at hand.****
>> - Conal****
>> ** **
>> -- Conal****
>>
>> ** **
>> On Sat, Sep 28, 2013 at 9:57 PM, Edward Kmett <ekmett at gmail.com> wrote:**
>> **
>>
>> As part of the discussion about Typeable, GHC 7.8 is going to include a
>> Data.Type.Equality module that provides a polykinded type equality data
>> type.****
>> ** **
>> I'd like to propose that we rename this type to (==) rather than the
>> (:=:) it was developed under. ****
>> ** **
>> We are already using (+), (-), (*), etc. at the type level in type-nats,
>> so it would seem to fit the surrounding convention.****
>>  ****
>> I've done the work of preparing a patch, visible here:****
>> ** **
>>
>> https://github.com/ekmett/packages-base/commit/fb47f8368ad3d40fdd79bdeec334c0554fb17110
>> ****
>> ** **
>> Thoughts?****
>> ** **
>> Normally, I'd let this run the usual 2 week course, but we're getting
>> down to the wire for 7.8's release. Once 7.8 ships, we'd basically be stuck
>> with the current name forever.****
>> ** **
>> Discussion Period: 1 week****
>> ** **
>> -Edward Kmett****
>>
>>
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://www.haskell.org/mailman/listinfo/libraries****
>>
>> ** **
>>
>> ** **
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://www.haskell.org/mailman/listinfo/libraries****
>>
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20131011/7966fb0b/attachment-0001.html>