[Proposal] Renaming (:=:) to (==)
Edward Kmett
ekmett
Fri Oct 11 19:54:35 UTC 2013
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/9ee8e603/attachment-0001.html>
More information about the Libraries
mailing list