RFC: Singleton equality witnesses

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
15 messages Options
Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

Gabor Greif-2
Richard and all,

sorry for reviving such an ancient thread, but I'd like to move this
forward a bit :-)

In the meantime Iavor has added the (:~:) GADT, so I can reuse it. It
has been commented that it could (finally) end up in GHC.Exts, but for
now I want my changes minimized.

I have added the class @SingEquality@ and have implemented the
@sameSing@ method in terms of Iavor's functions. This is rather pretty
now. Here is the patch:

------------------------------------------------------
$ git show 0eacf265255b9c5e0191b6a5100f3076b8eb5520
commit 0eacf265255b9c5e0191b6a5100f3076b8eb5520
Author: Gabor Greif <ggreif at gmail.com>
Date:   Fri Nov 30 12:23:28 2012 +0100

    Introduce the SingEquality class
    with customizable witness type
    and a sameSing method that may
    produce the latter.

diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
index f8b759e..5546a5a 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -30,7 +30,7 @@ module GHC.TypeLits
   , type (-)

     -- * Comparing for equality
-  , type (:~:) (..), eqSingNat, eqSingSym
+  , type (:~:) (..), eqSingNat, eqSingSym, SingEquality (..)

     -- * Destructing type-nat singletons.
   , isZero, IsZero(..)
@@ -56,6 +56,7 @@ import Unsafe.Coerce(unsafeCoerce)
 -- import Data.Bits(testBit,shiftR)
 import Data.Maybe(Maybe(..))
 import Data.List((++))
+import Control.Monad (guard, return, (>>))

 -- | (Kind) A kind useful for passing kinds as parameters.
 data OfKind (a :: *) = KindParam
@@ -133,6 +134,11 @@ class (kparam ~ KindParam) => SingE (kparam ::
OfKind k) where
   type DemoteRep kparam :: *
   fromSing :: Sing (a :: k) -> DemoteRep kparam

+class (kparam ~ KindParam, SingE (kparam :: OfKind k)) =>
SingEquality (kparam :: OfKind k) where
+  type SameSing kparam :: k -> k -> *
+  type SameSing kparam = (:~:)
+  sameSing :: Sing a -> Sing b -> Maybe (SameSing kparam a b)
+
 instance SingE (KindParam :: OfKind Nat) where
   type DemoteRep (KindParam :: OfKind Nat) = Integer
   fromSing (SNat n) = n
@@ -141,6 +147,12 @@ instance SingE (KindParam :: OfKind Symbol) where
   type DemoteRep (KindParam :: OfKind Symbol) = String
   fromSing (SSym s) = s

+instance SingEquality (KindParam :: OfKind Nat) where
+  sameSing = eqSingNat
+
+instance SingEquality (KindParam :: OfKind Symbol) where
+  sameSing = eqSingSym
+
 {- | A convenient name for the type used to representing the values
 for a particular singleton family.  For example, @Demote 2 ~ Integer@,
 and also @Demote 3 ~ Integer@, but @Demote "Hello" ~ String at . -}
------------------------------------------------------

Regarding Richard's decidable equality suggestion, I think this would
be the next step. IIRC, empty case expressions have been implemented,
so GHC HEAD should be prepared.

What do you think? Okay to push in this form?

Cheers,

    Gabor


On 12/5/12, Richard Eisenberg <eir at cis.upenn.edu> wrote:

> I don't think anything here is *high priority*, just musings on how best to
> move forward.
>
> About empty case, consider this:
>
>> data a :~: b where
>>   Refl :: a :~: a
>>
>> absurd :: True :~: False -> a
>
> Now, I want to write a term binding for absurd. GHC can figure out that
> (True :~: False) is an empty type. So, if we have (absurd x = case x of ?),
> there are no valid patterns, other than _, that could be used. Instead of
> writing (absurd _ = undefined), I would much prefer to write (absurd x =
> case x of {}). Why? If I compile with -fwarn-incomplete-patterns and
> -Werror, then the latter has no possible source of partiality and yet
> compiles. The former looks dangerous, and GHC doesn't check to make sure
> that, in fact, the function can never get called.
>
> The bottom line, for me at least, is that I want to avoid the partial
> constructs (incomplete patterns, undefined, etc) in Haskell as much as
> possible, especially when I'm leveraging the type system to a high degree.
> The lack of empty case statements forces me to use undefined where it isn't
> really necessary.
>
> I'll leave it to others to comment on TypeRep, as I'm a little hazy there
> myself.
>
> Richard
>
>


Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

Richard Eisenberg-2
I'm glad you've revived the thread, Gabor. My attention has been diverted elsewhere, but it's good to move forward with this. Thanks.

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 easily be redefined into any empty type.) You're right that empty pattern matches are available now (thanks, Simon!) but their usefulness comes into play only with the Either type, not with the Maybe type. What you have below would certainly be useful, but in my opinion, the Either construction is more so.

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 (:~:)?

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!

Richard

On Feb 5, 2013, at 1:34 PM, Gabor Greif <ggreif at gmail.com> wrote:

> Richard and all,
>
> sorry for reviving such an ancient thread, but I'd like to move this
> forward a bit :-)
>
> In the meantime Iavor has added the (:~:) GADT, so I can reuse it. It
> has been commented that it could (finally) end up in GHC.Exts, but for
> now I want my changes minimized.
>
> I have added the class @SingEquality@ and have implemented the
> @sameSing@ method in terms of Iavor's functions. This is rather pretty
> now. Here is the patch:
>
> ------------------------------------------------------
> $ git show 0eacf265255b9c5e0191b6a5100f3076b8eb5520
> commit 0eacf265255b9c5e0191b6a5100f3076b8eb5520
> Author: Gabor Greif <ggreif at gmail.com>
> Date:   Fri Nov 30 12:23:28 2012 +0100
>
>    Introduce the SingEquality class
>    with customizable witness type
>    and a sameSing method that may
>    produce the latter.
>
> diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
> index f8b759e..5546a5a 100644
> --- a/GHC/TypeLits.hs
> +++ b/GHC/TypeLits.hs
> @@ -30,7 +30,7 @@ module GHC.TypeLits
>   , type (-)
>
>     -- * Comparing for equality
> -  , type (:~:) (..), eqSingNat, eqSingSym
> +  , type (:~:) (..), eqSingNat, eqSingSym, SingEquality (..)
>
>     -- * Destructing type-nat singletons.
>   , isZero, IsZero(..)
> @@ -56,6 +56,7 @@ import Unsafe.Coerce(unsafeCoerce)
> -- import Data.Bits(testBit,shiftR)
> import Data.Maybe(Maybe(..))
> import Data.List((++))
> +import Control.Monad (guard, return, (>>))
>
> -- | (Kind) A kind useful for passing kinds as parameters.
> data OfKind (a :: *) = KindParam
> @@ -133,6 +134,11 @@ class (kparam ~ KindParam) => SingE (kparam ::
> OfKind k) where
>   type DemoteRep kparam :: *
>   fromSing :: Sing (a :: k) -> DemoteRep kparam
>
> +class (kparam ~ KindParam, SingE (kparam :: OfKind k)) =>
> SingEquality (kparam :: OfKind k) where
> +  type SameSing kparam :: k -> k -> *
> +  type SameSing kparam = (:~:)
> +  sameSing :: Sing a -> Sing b -> Maybe (SameSing kparam a b)
> +
> instance SingE (KindParam :: OfKind Nat) where
>   type DemoteRep (KindParam :: OfKind Nat) = Integer
>   fromSing (SNat n) = n
> @@ -141,6 +147,12 @@ instance SingE (KindParam :: OfKind Symbol) where
>   type DemoteRep (KindParam :: OfKind Symbol) = String
>   fromSing (SSym s) = s
>
> +instance SingEquality (KindParam :: OfKind Nat) where
> +  sameSing = eqSingNat
> +
> +instance SingEquality (KindParam :: OfKind Symbol) where
> +  sameSing = eqSingSym
> +
> {- | A convenient name for the type used to representing the values
> for a particular singleton family.  For example, @Demote 2 ~ Integer@,
> and also @Demote 3 ~ Integer@, but @Demote "Hello" ~ String at . -}
> ------------------------------------------------------
>
> Regarding Richard's decidable equality suggestion, I think this would
> be the next step. IIRC, empty case expressions have been implemented,
> so GHC HEAD should be prepared.
>
> What do you think? Okay to push in this form?
>
> Cheers,
>
>    Gabor
>
>
> On 12/5/12, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>> I don't think anything here is *high priority*, just musings on how best to
>> move forward.
>>
>> About empty case, consider this:
>>
>>> data a :~: b where
>>>  Refl :: a :~: a
>>>
>>> absurd :: True :~: False -> a
>>
>> Now, I want to write a term binding for absurd. GHC can figure out that
>> (True :~: False) is an empty type. So, if we have (absurd x = case x of ?),
>> there are no valid patterns, other than _, that could be used. Instead of
>> writing (absurd _ = undefined), I would much prefer to write (absurd x =
>> case x of {}). Why? If I compile with -fwarn-incomplete-patterns and
>> -Werror, then the latter has no possible source of partiality and yet
>> compiles. The former looks dangerous, and GHC doesn't check to make sure
>> that, in fact, the function can never get called.
>>
>> The bottom line, for me at least, is that I want to avoid the partial
>> constructs (incomplete patterns, undefined, etc) in Haskell as much as
>> possible, especially when I'm leveraging the type system to a high degree.
>> The lack of empty case statements forces me to use undefined where it isn't
>> really necessary.
>>
>> I'll leave it to others to comment on TypeRep, as I'm a little hazy there
>> myself.
>>
>> Richard
>>
>>
>



Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

Gabor Greif-2
On 2/5/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> I'm glad you've revived the thread, Gabor. My attention has been diverted
> elsewhere, but it's good to move forward with this. Thanks.

Hi Richard,

thanks for the encouragement!

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

So I decided to leave 'sameSing' in and add a new method 'decideSing'
with your semantics. However, I have no idea how to implement the
non-equality pieces of Nat and Symbol. I have punted for now, failing
to add the corresponding branches. Maybe you can come up with
something sensible. Anyway, sameSing now has a default method that
maps positive evidence from decideSing into the Maybe monad.
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. (This is not a political
message, though :-)

> easily be redefined into any empty type.) You're right that empty pattern
> matches are available now (thanks, Simon!) but their usefulness comes into
> play only with the Either type, not with the Maybe type. What you have below
> would certainly be useful, but in my opinion, the Either construction is
> more so.
>
> 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).

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


Okay, here is the diff that I have so far:

-------------------------------------------------------------------
index f8b759e..7715a32 100644
--- a/GHC/TypeLits.hs
+++ b/GHC/TypeLits.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE TypeFamilies #-}           -- for declaring operators +
sing family
 {-# LANGUAGE TypeOperators #-}          -- for declaring operator
 {-# LANGUAGE EmptyDataDecls #-}         -- for declaring the kinds
+{-# LANGUAGE EmptyCase #-}              -- for absurd
 {-# LANGUAGE GADTs #-}                  -- for examining type nats
 {-# LANGUAGE PolyKinds #-}              -- for Sing family
 {-# LANGUAGE FlexibleContexts #-}
@@ -30,7 +31,7 @@ module GHC.TypeLits
   , type (-)

     -- * Comparing for equality
-  , type (:~:) (..), eqSingNat, eqSingSym
+  , type (:~:) (..), eqSingNat, eqSingSym, SingEquality (..)

     -- * Destructing type-nat singletons.
   , isZero, IsZero(..)
@@ -56,6 +57,8 @@ import Unsafe.Coerce(unsafeCoerce)
 -- import Data.Bits(testBit,shiftR)
 import Data.Maybe(Maybe(..))
 import Data.List((++))
+import Data.Either(Either (..))
+import Control.Monad (guard, return, (>>))

 -- | (Kind) A kind useful for passing kinds as parameters.
 data OfKind (a :: *) = KindParam
@@ -133,6 +136,15 @@ class (kparam ~ KindParam) => SingE (kparam ::
OfKind k) where
   type DemoteRep kparam :: *
   fromSing :: Sing (a :: k) -> DemoteRep kparam

+class (kparam ~ KindParam, SingE (kparam :: OfKind k)) =>
SingEquality (kparam :: OfKind k) where
+  type SameSing kparam :: k -> k -> *
+  type SameSing kparam = (:~:)
+  sameSing :: Sing a -> Sing b -> Maybe (SameSing kparam a b)
+  sameSing a b = case decideSing a b of
+                 Right witness -> Just witness
+                 otherwise -> Nothing
+  decideSing :: Sing a -> Sing b -> Decision (SameSing kparam a b)
+
 instance SingE (KindParam :: OfKind Nat) where
   type DemoteRep (KindParam :: OfKind Nat) = Integer
   fromSing (SNat n) = n
@@ -141,6 +153,16 @@ instance SingE (KindParam :: OfKind Symbol) where
   type DemoteRep (KindParam :: OfKind Symbol) = String
   fromSing (SSym s) = s

+instance SingEquality (KindParam :: OfKind Nat) where
+  sameSing = eqSingNat
+  decideSing a b = case eqSingNat a b of
+                   Just witness -> Right witness
+
+instance SingEquality (KindParam :: OfKind Symbol) where
+  sameSing = eqSingSym
+  decideSing a b = case eqSingSym a b of
+                   Just witness -> Right witness
+
 {- | A convenient name for the type used to representing the values
 for a particular singleton family.  For example, @Demote 2 ~ Integer@,
 and also @Demote 3 ~ Integer@, but @Demote "Hello" ~ String at . -}
@@ -236,6 +258,18 @@ data (:~:) :: k -> k -> * where
 instance Show (a :~: b) where
   show Refl = "Refl"

+
+-- | A type that has no inhabitants.
+data Void
+
+-- | Anything follow from falseness.
+absurd :: Void -> a
+absurd x = case x of {}
+
+type Refuted a = a -> Void
+
+type Decision a = Either (Refuted a) a
+
 {- | Check if two type-natural singletons of potentially different types
 are indeed the same, by comparing their runtime representations.
-------------------------------------------------------------------

I haven't exported all parts yet.

What do you think?

Cheers,

    Gabor

>
> Richard
>
> On Feb 5, 2013, at 1:34 PM, Gabor Greif <ggreif at gmail.com> wrote:
>
>> Richard and all,
>>
>> sorry for reviving such an ancient thread, but I'd like to move this
>> forward a bit :-)
>>
>> In the meantime Iavor has added the (:~:) GADT, so I can reuse it. It
>> has been commented that it could (finally) end up in GHC.Exts, but for
>> now I want my changes minimized.
>>
>> I have added the class @SingEquality@ and have implemented the
>> @sameSing@ method in terms of Iavor's functions. This is rather pretty
>> now. Here is the patch:
>>
>> ------------------------------------------------------
>> $ git show 0eacf265255b9c5e0191b6a5100f3076b8eb5520
>> commit 0eacf265255b9c5e0191b6a5100f3076b8eb5520
>> Author: Gabor Greif <ggreif at gmail.com>
>> Date:   Fri Nov 30 12:23:28 2012 +0100
>>
>>    Introduce the SingEquality class
>>    with customizable witness type
>>    and a sameSing method that may
>>    produce the latter.
>>
>> diff --git a/GHC/TypeLits.hs b/GHC/TypeLits.hs
>> index f8b759e..5546a5a 100644
>> --- a/GHC/TypeLits.hs
>> +++ b/GHC/TypeLits.hs
>> @@ -30,7 +30,7 @@ module GHC.TypeLits
>>   , type (-)
>>
>>     -- * Comparing for equality
>> -  , type (:~:) (..), eqSingNat, eqSingSym
>> +  , type (:~:) (..), eqSingNat, eqSingSym, SingEquality (..)
>>
>>     -- * Destructing type-nat singletons.
>>   , isZero, IsZero(..)
>> @@ -56,6 +56,7 @@ import Unsafe.Coerce(unsafeCoerce)
>> -- import Data.Bits(testBit,shiftR)
>> import Data.Maybe(Maybe(..))
>> import Data.List((++))
>> +import Control.Monad (guard, return, (>>))
>>
>> -- | (Kind) A kind useful for passing kinds as parameters.
>> data OfKind (a :: *) = KindParam
>> @@ -133,6 +134,11 @@ class (kparam ~ KindParam) => SingE (kparam ::
>> OfKind k) where
>>   type DemoteRep kparam :: *
>>   fromSing :: Sing (a :: k) -> DemoteRep kparam
>>
>> +class (kparam ~ KindParam, SingE (kparam :: OfKind k)) =>
>> SingEquality (kparam :: OfKind k) where
>> +  type SameSing kparam :: k -> k -> *
>> +  type SameSing kparam = (:~:)
>> +  sameSing :: Sing a -> Sing b -> Maybe (SameSing kparam a b)
>> +
>> instance SingE (KindParam :: OfKind Nat) where
>>   type DemoteRep (KindParam :: OfKind Nat) = Integer
>>   fromSing (SNat n) = n
>> @@ -141,6 +147,12 @@ instance SingE (KindParam :: OfKind Symbol) where
>>   type DemoteRep (KindParam :: OfKind Symbol) = String
>>   fromSing (SSym s) = s
>>
>> +instance SingEquality (KindParam :: OfKind Nat) where
>> +  sameSing = eqSingNat
>> +
>> +instance SingEquality (KindParam :: OfKind Symbol) where
>> +  sameSing = eqSingSym
>> +
>> {- | A convenient name for the type used to representing the values
>> for a particular singleton family.  For example, @Demote 2 ~ Integer@,
>> and also @Demote 3 ~ Integer@, but @Demote "Hello" ~ String at . -}
>> ------------------------------------------------------
>>
>> Regarding Richard's decidable equality suggestion, I think this would
>> be the next step. IIRC, empty case expressions have been implemented,
>> so GHC HEAD should be prepared.
>>
>> What do you think? Okay to push in this form?
>>
>> Cheers,
>>
>>    Gabor
>>
>>
>> On 12/5/12, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>>> I don't think anything here is *high priority*, just musings on how best
>>> to
>>> move forward.
>>>
>>> About empty case, consider this:
>>>
>>>> data a :~: b where
>>>>  Refl :: a :~: a
>>>>
>>>> absurd :: True :~: False -> a
>>>
>>> Now, I want to write a term binding for absurd. GHC can figure out that
>>> (True :~: False) is an empty type. So, if we have (absurd x = case x of
>>> ?),
>>> there are no valid patterns, other than _, that could be used. Instead
>>> of
>>> writing (absurd _ = undefined), I would much prefer to write (absurd x =
>>> case x of {}). Why? If I compile with -fwarn-incomplete-patterns and
>>> -Werror, then the latter has no possible source of partiality and yet
>>> compiles. The former looks dangerous, and GHC doesn't check to make sure
>>> that, in fact, the function can never get called.
>>>
>>> The bottom line, for me at least, is that I want to avoid the partial
>>> constructs (incomplete patterns, undefined, etc) in Haskell as much as
>>> possible, especially when I'm leveraging the type system to a high
>>> degree.
>>> The lack of empty case statements forces me to use undefined where it
>>> isn't
>>> really necessary.
>>>
>>> I'll leave it to others to comment on TypeRep, as I'm a little hazy
>>> there
>>> myself.
>>>
>>> Richard
>>>
>>>
>>
>
>


Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

Richard Eisenberg-2

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.

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

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

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

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?

Richard

Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

Gabor Greif-2
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


Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

José Pedro Magalhães
On Wed, Feb 6, 2013 at 7:17 PM, Gabor Greif <ggreif at gmail.com> wrote:

> On 2/6/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> > 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).
>

Can you perhaps summarise exactly what needs to be added to GHC for this to
work?
It's not immediately clear to me why this is not just a library issue.


Thanks,
Pedro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130207/c174f121/attachment.htm>

Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

Gabor Greif-2
Oi Jos?,

this is a library-only issue, the branch is in libraries/base, thus
somewhat tied to the 7.8 release.

Cheers,

    Gabor

On 2/7/13, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote:

> On Wed, Feb 6, 2013 at 7:17 PM, Gabor Greif <ggreif at gmail.com> wrote:
>
>> On 2/6/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>> > 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).
>>
>
> Can you perhaps summarise exactly what needs to be added to GHC for this to
> work?
> It's not immediately clear to me why this is not just a library issue.
>
>
> Thanks,
> Pedro
>


Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

José Pedro Magalhães
Hey Gabor,

And why should it be part of base? Don't get me wrong, I'm not saying this
is not important/useful. I'm just wondering about the reason to have it in
base.
Is it tied to TypeLits?


Cheers,
Pedro

On Thu, Feb 7, 2013 at 2:21 PM, Gabor Greif <ggreif at gmail.com> wrote:

> Oi Jos?,
>
> this is a library-only issue, the branch is in libraries/base, thus
> somewhat tied to the 7.8 release.
>
> Cheers,
>
>     Gabor
>
> On 2/7/13, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote:
> > On Wed, Feb 6, 2013 at 7:17 PM, Gabor Greif <ggreif at gmail.com> wrote:
> >
> >> On 2/6/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> >> > 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).
> >>
> >
> > Can you perhaps summarise exactly what needs to be added to GHC for this
> to
> > work?
> > It's not immediately clear to me why this is not just a library issue.
> >
> >
> > Thanks,
> > Pedro
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130207/e1b489d0/attachment-0001.htm>

Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

Gabor Greif-2
In its current state it is not tied to TypeLits, but when Richard adds
his magic it probably will be. It is still an open issue where to put
what, and whether a new module would be fitting.
Richard surely will comment on this. I'd prefer the new instance
definitions in TypeLits to avoid orphans. Thanks for your input
though, this is exactly the kind of feedback we were hoping for :-)

Cheers,

    Gabor


[looks like I lost a previous version of this response, sorry if you
get it twice]

On 2/7/13, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote:

> Hey Gabor,
>
> And why should it be part of base? Don't get me wrong, I'm not saying this
> is not important/useful. I'm just wondering about the reason to have it in
> base.
> Is it tied to TypeLits?
>
>
> Cheers,
> Pedro
>
> On Thu, Feb 7, 2013 at 2:21 PM, Gabor Greif <ggreif at gmail.com> wrote:
>
>> Oi Jos?,
>>
>> this is a library-only issue, the branch is in libraries/base, thus
>> somewhat tied to the 7.8 release.
>>
>> Cheers,
>>
>>     Gabor
>>
>> On 2/7/13, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote:
>> > On Wed, Feb 6, 2013 at 7:17 PM, Gabor Greif <ggreif at gmail.com> wrote:
>> >
>> >> On 2/6/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>> >> > 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).
>> >>
>> >
>> > Can you perhaps summarise exactly what needs to be added to GHC for
>> > this
>> to
>> > work?
>> > It's not immediately clear to me why this is not just a library issue.
>> >
>> >
>> > Thanks,
>> > Pedro
>> >
>>
>


Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

Iavor Diatchki
Hello,

my preference would be to build this kind of functionality (and other
related features) in libraries on top of GHC.TypeLits.  This modules was
intended to contain only a minimal set of the constants that the compiler
needs to know about, and it already may have too much in it.

On the concrete issue:  orphan instances could be avoided if the type lits
instances are defined in the same module as the class.

-Iavor


On Thu, Feb 7, 2013 at 6:50 AM, Gabor Greif <ggreif at gmail.com> wrote:

> In its current state it is not tied to TypeLits, but when Richard adds
> his magic it probably will be. It is still an open issue where to put
> what, and whether a new module would be fitting.
> Richard surely will comment on this. I'd prefer the new instance
> definitions in TypeLits to avoid orphans. Thanks for your input
> though, this is exactly the kind of feedback we were hoping for :-)
>
> Cheers,
>
>     Gabor
>
>
> [looks like I lost a previous version of this response, sorry if you
> get it twice]
>
> On 2/7/13, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote:
> > Hey Gabor,
> >
> > And why should it be part of base? Don't get me wrong, I'm not saying
> this
> > is not important/useful. I'm just wondering about the reason to have it
> in
> > base.
> > Is it tied to TypeLits?
> >
> >
> > Cheers,
> > Pedro
> >
> > On Thu, Feb 7, 2013 at 2:21 PM, Gabor Greif <ggreif at gmail.com> wrote:
> >
> >> Oi Jos?,
> >>
> >> this is a library-only issue, the branch is in libraries/base, thus
> >> somewhat tied to the 7.8 release.
> >>
> >> Cheers,
> >>
> >>     Gabor
> >>
> >> On 2/7/13, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote:
> >> > On Wed, Feb 6, 2013 at 7:17 PM, Gabor Greif <ggreif at gmail.com> wrote:
> >> >
> >> >> On 2/6/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> >> >> > 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).
> >> >>
> >> >
> >> > Can you perhaps summarise exactly what needs to be added to GHC for
> >> > this
> >> to
> >> > work?
> >> > It's not immediately clear to me why this is not just a library issue.
> >> >
> >> >
> >> > Thanks,
> >> > Pedro
> >> >
> >>
> >
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130207/2c5071ed/attachment-0001.htm>

Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

Richard Eisenberg-2
I've just pushed a commit to the type-reasoning branch with a strawman proposal of a reorganization of these definitions. Specifically, this commit breaks TypeLits into the following five files:

- GHC.TypeEq, which contains the definitions for (:~:), Void, Refuted, etc.
- GHC.Singletons, which contains the definitions about singletons in general, such as SingI and SingEquality
- GHC.TypeLits.Unsafe, which contains just unsafeSingNat and unsafeSingSymbol
- GHC.TypeLits.Internals, which is necessary to get GHC.TypeLits.Unsafe to have access to the right internals;
this module is not exported from the 'base' package
and
- GHC.TypeLits, which contains the definitions specific to type-level literals.

Some thoughts on this design:
- First off, why is TypeEq part of GHC?? Because we wish to write eqSingNat and eqSingSym in GHC.TypeLits, and that module rightly deserves to be part of GHC. I'm quite uncomfortable with this decision, and I even created a new git repo at github.com/goldfirere/type-reasoning to hold the definitions that eventually ended up in GHC.TypeEq. (The repo has nothing in it, now.) Perhaps the best resolution is to move eqSingNat and eqSingSym out of GHC.TypeLits and into an external package, but that seems silly in a different direction. (It is fully technically feasible, as those functions don't depend on any internals.) I would love some feedback here.
- Why is Singletons broken off? No strong reason here, but it seemed that the singletons-oriented definitions weren't solely related to type-level literals, so it seemed more natural this way.
- Making the Unsafe module was a little more principled, because those functions really are unsafe! They are quite useful, though, and should be available somewhere.
- Currently, the internals of GHC assign types like "0" the kind GHC.TypeLits.Nat, so Nat and Symbol *must* remain in the GHC.TypeLits module. Unfortunately, the plumbing around GHC.TypeLits.Unsafe want Nat and Symbol to be defined in GHC.TypeLits.Internals. So, I created a TypeLits.hs-boot file to fix the problem. This is highly unsatisfactory, and if something like what I've done here sticks around, we should change the internals of GHC to use GHC.TypeLits.Internals.Nat, getting rid of the import cycle.
- I've put in the decideSing function as discussed further up in this thread. Its implementation for Nat and Symbol must use unsafeCoerce, but that shouldn't be a surprise.

Unfortunately, the code doesn't compile now. This is because it needs SingI instances for, say, Sing 0. For a reason I have not explored, these instances are not available here, though they seem to be for code written outside of GHC. Iavor, any thoughts on this?

Please tear any of these ideas (or my whole commit) to shreds! It really is meant to be a strawman proposal, but committing these changes seemed the best way of communicating on possible set of design decisions.

Richard

PS: I'm pasting much of this email to the wiki page for posterity.

On Feb 7, 2013, at 10:45 AM, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:

> Hello,
>
> my preference would be to build this kind of functionality (and other related features) in libraries on top of GHC.TypeLits.  This modules was intended to contain only a minimal set of the constants that the compiler needs to know about, and it already may have too much in it.
>
> On the concrete issue:  orphan instances could be avoided if the type lits instances are defined in the same module as the class.
>
> -Iavor
>
>
> On Thu, Feb 7, 2013 at 6:50 AM, Gabor Greif <ggreif at gmail.com> wrote:
> In its current state it is not tied to TypeLits, but when Richard adds
> his magic it probably will be. It is still an open issue where to put
> what, and whether a new module would be fitting.
> Richard surely will comment on this. I'd prefer the new instance
> definitions in TypeLits to avoid orphans. Thanks for your input
> though, this is exactly the kind of feedback we were hoping for :-)
>
> Cheers,
>
>     Gabor
>
>
> [looks like I lost a previous version of this response, sorry if you
> get it twice]
>
> On 2/7/13, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote:
> > Hey Gabor,
> >
> > And why should it be part of base? Don't get me wrong, I'm not saying this
> > is not important/useful. I'm just wondering about the reason to have it in
> > base.
> > Is it tied to TypeLits?
> >
> >
> > Cheers,
> > Pedro
> >
> > On Thu, Feb 7, 2013 at 2:21 PM, Gabor Greif <ggreif at gmail.com> wrote:
> >
> >> Oi Jos?,
> >>
> >> this is a library-only issue, the branch is in libraries/base, thus
> >> somewhat tied to the 7.8 release.
> >>
> >> Cheers,
> >>
> >>     Gabor
> >>
> >> On 2/7/13, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote:
> >> > On Wed, Feb 6, 2013 at 7:17 PM, Gabor Greif <ggreif at gmail.com> wrote:
> >> >
> >> >> On 2/6/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> >> >> > 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).
> >> >>
> >> >
> >> > Can you perhaps summarise exactly what needs to be added to GHC for
> >> > this
> >> to
> >> > work?
> >> > It's not immediately clear to me why this is not just a library issue.
> >> >
> >> >
> >> > Thanks,
> >> > Pedro
> >> >
> >>
> >
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130211/12d59fac/attachment-0001.htm>

Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

Simon Peyton Jones
- Currently, the internals of GHC assign types like "0" the kind GHC.TypeLits.Nat, so Nat and Symbol *must* remain in the GHC.TypeLits module. Unfortunately, the plumbing around GHC.TypeLits.Unsafe want Nat and Symbol to be defined in GHC.TypeLits.Internals. So, I created a TypeLits.hs-boot file to fix the problem. This is highly unsatisfactory, and if something like what I've done here sticks around, we should change the internals of GHC to use GHC.TypeLits.Internals.Nat, getting rid of the import cycle.

Let's NOT have an hs-boot file here.  Instead, change PrelNames to tell GHC where Nat and Symbol are defined.  It's ok for them to be in Internals.

I'm also unconvinced about the distinction between "Internals" and "Unsafe".  To me the former connotes the latter.  Import Internals if you know what you are doing; eg that might let you break important invariants.  Import a kosher module like TypeLits if you want the Joe Programmer interface.

Simon

From: ghc-devs-bounces at haskell.org [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Richard Eisenberg
Sent: 12 February 2013 02:41
To: Iavor Diatchki
Cc: Jos? Pedro Magalh?es; ghc-devs
Subject: Re: RFC: Singleton equality witnesses

I've just pushed a commit to the type-reasoning branch with a strawman proposal of a reorganization of these definitions. Specifically, this commit breaks TypeLits into the following five files:

- GHC.TypeEq, which contains the definitions for (:~:), Void, Refuted, etc.
- GHC.Singletons, which contains the definitions about singletons in general, such as SingI and SingEquality
- GHC.TypeLits.Unsafe, which contains just unsafeSingNat and unsafeSingSymbol
- GHC.TypeLits.Internals, which is necessary to get GHC.TypeLits.Unsafe to have access to the right internals;
this module is not exported from the 'base' package
and
- GHC.TypeLits, which contains the definitions specific to type-level literals.

Some thoughts on this design:
- First off, why is TypeEq part of GHC?? Because we wish to write eqSingNat and eqSingSym in GHC.TypeLits, and that module rightly deserves to be part of GHC. I'm quite uncomfortable with this decision, and I even created a new git repo at github.com/goldfirere/type-reasoning<http://github.com/goldfirere/type-reasoning> to hold the definitions that eventually ended up in GHC.TypeEq. (The repo has nothing in it, now.) Perhaps the best resolution is to move eqSingNat and eqSingSym out of GHC.TypeLits and into an external package, but that seems silly in a different direction. (It is fully technically feasible, as those functions don't depend on any internals.) I would love some feedback here.
- Why is Singletons broken off? No strong reason here, but it seemed that the singletons-oriented definitions weren't solely related to type-level literals, so it seemed more natural this way.
- Making the Unsafe module was a little more principled, because those functions really are unsafe! They are quite useful, though, and should be available somewhere.
- Currently, the internals of GHC assign types like "0" the kind GHC.TypeLits.Nat, so Nat and Symbol *must* remain in the GHC.TypeLits module. Unfortunately, the plumbing around GHC.TypeLits.Unsafe want Nat and Symbol to be defined in GHC.TypeLits.Internals. So, I created a TypeLits.hs-boot file to fix the problem. This is highly unsatisfactory, and if something like what I've done here sticks around, we should change the internals of GHC to use GHC.TypeLits.Internals.Nat, getting rid of the import cycle.
- I've put in the decideSing function as discussed further up in this thread. Its implementation for Nat and Symbol must use unsafeCoerce, but that shouldn't be a surprise.

Unfortunately, the code doesn't compile now. This is because it needs SingI instances for, say, Sing 0. For a reason I have not explored, these instances are not available here, though they seem to be for code written outside of GHC. Iavor, any thoughts on this?

Please tear any of these ideas (or my whole commit) to shreds! It really is meant to be a strawman proposal, but committing these changes seemed the best way of communicating on possible set of design decisions.

Richard

PS: I'm pasting much of this email to the wiki page for posterity.

On Feb 7, 2013, at 10:45 AM, Iavor Diatchki <iavor.diatchki at gmail.com<mailto:iavor.diatchki at gmail.com>> wrote:


Hello,

my preference would be to build this kind of functionality (and other related features) in libraries on top of GHC.TypeLits.  This modules was intended to contain only a minimal set of the constants that the compiler needs to know about, and it already may have too much in it.

On the concrete issue:  orphan instances could be avoided if the type lits instances are defined in the same module as the class.

-Iavor

On Thu, Feb 7, 2013 at 6:50 AM, Gabor Greif <ggreif at gmail.com<mailto:ggreif at gmail.com>> wrote:
In its current state it is not tied to TypeLits, but when Richard adds
his magic it probably will be. It is still an open issue where to put
what, and whether a new module would be fitting.
Richard surely will comment on this. I'd prefer the new instance
definitions in TypeLits to avoid orphans. Thanks for your input
though, this is exactly the kind of feedback we were hoping for :-)

Cheers,

    Gabor


[looks like I lost a previous version of this response, sorry if you
get it twice]

On 2/7/13, Jos? Pedro Magalh?es <jpm at cs.uu.nl<mailto:jpm at cs.uu.nl>> wrote:

> Hey Gabor,
>
> And why should it be part of base? Don't get me wrong, I'm not saying this
> is not important/useful. I'm just wondering about the reason to have it in
> base.
> Is it tied to TypeLits?
>
>
> Cheers,
> Pedro
>
> On Thu, Feb 7, 2013 at 2:21 PM, Gabor Greif <ggreif at gmail.com<mailto:ggreif at gmail.com>> wrote:
>
>> Oi Jos?,
>>
>> this is a library-only issue, the branch is in libraries/base, thus
>> somewhat tied to the 7.8 release.
>>
>> Cheers,
>>
>>     Gabor
>>
>> On 2/7/13, Jos? Pedro Magalh?es <jpm at cs.uu.nl<mailto:jpm at cs.uu.nl>> wrote:
>> > On Wed, Feb 6, 2013 at 7:17 PM, Gabor Greif <ggreif at gmail.com<mailto:ggreif at gmail.com>> wrote:
>> >
>> >> On 2/6/13, Richard Eisenberg <eir at cis.upenn.edu<mailto:eir at cis.upenn.edu>> wrote:
>> >> > 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).
>> >>
>> >
>> > Can you perhaps summarise exactly what needs to be added to GHC for
>> > this
>> to
>> > work?
>> > It's not immediately clear to me why this is not just a library issue.
>> >
>> >
>> > Thanks,
>> > Pedro
>> >
>>
>
_______________________________________________
ghc-devs mailing list
ghc-devs at haskell.org<mailto:ghc-devs at haskell.org>
http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
ghc-devs at haskell.org<mailto:ghc-devs at haskell.org>
http://www.haskell.org/mailman/listinfo/ghc-devs

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130212/07309b58/attachment-0001.htm>

Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

Iavor Diatchki
Hi Richard,

Thanks for pushing on this!   The summary of my comments is this:  I think
that we should have 1 or 2 low-level (not necessarily safe) GHC modules
that contain all the bits that GHC needs to know about, and move all other
bits into a separate library, which is to be used by the actual users of
the system.  In this way, this library could evolve independently of GHC
releases.

Here are some more detailed comments:

On Mon, Feb 11, 2013 at 6:40 PM, Richard Eisenberg <eir at cis.upenn.edu>
 wrote:

> I've just pushed a commit to the type-reasoning branch with a strawman
> proposal of a reorganization of these definitions. Specifically, this
> commit breaks TypeLits into the following five files:
>
> - GHC.TypeEq, which contains the definitions for (:~:), Void, Refuted, etc.
> - GHC.Singletons, which contains the definitions about singletons in
> general, such as SingI and SingEquality
> - GHC.TypeLits.Unsafe, which contains just unsafeSingNat and
> unsafeSingSymbol
> - GHC.TypeLits.Internals, which is necessary to get GHC.TypeLits.Unsafe to
> have access to the right internals;
> this module is not exported from the 'base' package
> and
> - GHC.TypeLits, which contains the definitions specific to type-level
> literals.
>
> Like Simon, I think that there is no need to distinguish between
TypeList.Unsafe and TypeLits.Internals.

Some thoughts on this design:

> - First off, why is TypeEq part of GHC?? Because we wish to write
> eqSingNat and eqSingSym in GHC.TypeLits, and that module rightly deserves
> to be part of GHC. I'm quite uncomfortable with this decision, and I even
> created a new git repo at github.com/goldfirere/type-reasoning to hold
> the definitions that eventually ended up in GHC.TypeEq. (The repo has
> nothing in it, now.) Perhaps the best resolution is to move eqSingNat and
> eqSingSym out of GHC.TypeLits and into an external package, but that seems
> silly in a different direction. (It is fully technically feasible, as those
> functions don't depend on any internals.) I would love some feedback here.
>

We could move these out of GHC: they are just defined using (a safe use of)
`unsafeCoerce`.  They just need to know about the equality type (:~:), so I
think they should be defined wherever the equality type is defined.

Also, an unrelated piece of advice:  try to keep down the use of type
synonyms---they make libraries seem complex.  For example, most programmers
would understand the type 'a -> Void', but when I see `Refuted a` I have to
go lookup its definition and check if there is something special about it.


> - Why is Singletons broken off? No strong reason here, but it seemed that
> the singletons-oriented definitions weren't solely related to type-level
> literals, so it seemed more natural this way.
>

I don't think this matters too much either way, but I would look for things
to remove from here and move to the programmer facing library.  For
example, why should `SingEquality` be there?  It is important for `SingI`
to be in GHC, because the instances for type-level literals are wired into
GHC: it expects the class to be in GHC.TypeLits (this is why moving the
class broke the instances, take a look in
`compiler/prelude/TysWiredIn.lhs`, indeed, `Nat` and `Symbol` are also
wired into GHC in the same module).


> - Making the Unsafe module was a little more principled, because those
> functions really are unsafe! They are quite useful, though, and should be
> available somewhere.
>

Yes, I think that we want to export these at least for the use by the
programmer facing library---it may choose not to re-export them.

-Iavor



On Tue, Feb 12, 2013 at 12:38 AM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

>  - Currently, the internals of GHC assign types like "0" the kind
> GHC.TypeLits.Nat, so Nat and Symbol *must* remain in the GHC.TypeLits
> module. Unfortunately, the plumbing around GHC.TypeLits.Unsafe want Nat and
> Symbol to be defined in GHC.TypeLits.Internals. So, I created a
> TypeLits.hs-boot file to fix the problem. This is highly unsatisfactory,
> and if something like what I've done here sticks around, we should change
> the internals of GHC to use GHC.TypeLits.Internals.Nat, getting rid of the
> import cycle.****
>
> ** **
>
> Let?s NOT have an hs-boot file here.  Instead, change PrelNames to tell
> GHC where Nat and Symbol are defined.  It?s ok for them to be in Internals.
> ****
>
> ** **
>
> I?m also unconvinced about the distinction between ?Internals? and
> ?Unsafe?.  To me the former connotes the latter.  Import Internals if you
> know what you are doing; eg that might let you break important invariants.
> Import a kosher module like TypeLits if you want the Joe Programmer
> interface.****
>
> ** **
>
> Simon****
>
> ** **
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130212/48f1c744/attachment.htm>

Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

Gabor Greif-2
In reply to this post by Richard Eisenberg-2
On 2/12/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:

> I've just pushed a commit to the type-reasoning branch with a strawman
> proposal of a reorganization of these definitions. Specifically, this commit
> breaks TypeLits into the following five files:
>
> - GHC.TypeEq, which contains the definitions for (:~:), Void, Refuted, etc.
> - GHC.Singletons, which contains the definitions about singletons in
> general, such as SingI and SingEquality
> - GHC.TypeLits.Unsafe, which contains just unsafeSingNat and
> unsafeSingSymbol
> - GHC.TypeLits.Internals, which is necessary to get GHC.TypeLits.Unsafe to
> have access to the right internals;
> this module is not exported from the 'base' package
> and
> - GHC.TypeLits, which contains the definitions specific to type-level
> literals.

As Simon said, having GHC.TypeLits.Unsafe and GHC.TypeLits.Internals
sounds like overkill, but it is similar to the other "unsafe"
functionality's whereabouts.
If we had an "export towards" feature then this division would make
perfect sense and users could only ever include GHC.TypeLits.Unsafe,
which should make their alarm bells ring. As I understand nobody
should include GHC.TypeLits.Internals (other than
GHC.TypeLits.Unsafe), but we cannot enforce that now. In light of this
I think it is okay to have two modules.

>
> Some thoughts on this design:
> - First off, why is TypeEq part of GHC?? Because we wish to write eqSingNat
> and eqSingSym in GHC.TypeLits, and that module rightly deserves to be part
> of GHC. I'm quite uncomfortable with this decision, and I even created a new
> git repo at github.com/goldfirere/type-reasoning to hold the definitions
> that eventually ended up in GHC.TypeEq. (The repo has nothing in it, now.)
> Perhaps the best resolution is to move eqSingNat and eqSingSym out of
> GHC.TypeLits and into an external package, but that seems silly in a
> different direction. (It is fully technically feasible, as those functions
> don't depend on any internals.) I would love some feedback here.

But doesn't the GHC type system need some inside knowledge of the Nat
and Symbol kinds?

> - Why is Singletons broken off? No strong reason here, but it seemed that
> the singletons-oriented definitions weren't solely related to type-level
> literals, so it seemed more natural this way.

I can understand this.

> - Making the Unsafe module was a little more principled, because those
> functions really are unsafe! They are quite useful, though, and should be
> available somewhere.
> - Currently, the internals of GHC assign types like "0" the kind
> GHC.TypeLits.Nat, so Nat and Symbol *must* remain in the GHC.TypeLits
> module. Unfortunately, the plumbing around GHC.TypeLits.Unsafe want Nat and
> Symbol to be defined in GHC.TypeLits.Internals. So, I created a
> TypeLits.hs-boot file to fix the problem. This is highly unsatisfactory, and
> if something like what I've done here sticks around, we should change the
> internals of GHC to use GHC.TypeLits.Internals.Nat, getting rid of the
> import cycle.
> - I've put in the decideSing function as discussed further up in this
> thread. Its implementation for Nat and Symbol must use unsafeCoerce, but
> that shouldn't be a surprise.

Great, hope to have a look at them soon.

>
> Unfortunately, the code doesn't compile now. This is because it needs SingI
> instances for, say, Sing 0. For a reason I have not explored, these
> instances are not available here, though they seem to be for code written
> outside of GHC. Iavor, any thoughts on this?
>
> Please tear any of these ideas (or my whole commit) to shreds! It really is
> meant to be a strawman proposal, but committing these changes seemed the
> best way of communicating on possible set of design decisions.

One thing i think is pretty much important, that I haven't seen
spelled out yet, is the "derive SingEquality" feature that can
probably be stacked upon all of this. After all, the decidable
equality should be rather mechanically derivable from any singleton
definition.

So overall, I like what I read here, of course the compilability
should be restored, but I cannot contribute at that end.

Thanks for the hard work, and cheers,

    Gabor


>
> Richard
>
> PS: I'm pasting much of this email to the wiki page for posterity.
>
> On Feb 7, 2013, at 10:45 AM, Iavor Diatchki <iavor.diatchki at gmail.com>
> wrote:
>
>> Hello,
>>
>> my preference would be to build this kind of functionality (and other
>> related features) in libraries on top of GHC.TypeLits.  This modules was
>> intended to contain only a minimal set of the constants that the compiler
>> needs to know about, and it already may have too much in it.
>>
>> On the concrete issue:  orphan instances could be avoided if the type lits
>> instances are defined in the same module as the class.
>>
>> -Iavor
>>
>>
>> On Thu, Feb 7, 2013 at 6:50 AM, Gabor Greif <ggreif at gmail.com> wrote:
>> In its current state it is not tied to TypeLits, but when Richard adds
>> his magic it probably will be. It is still an open issue where to put
>> what, and whether a new module would be fitting.
>> Richard surely will comment on this. I'd prefer the new instance
>> definitions in TypeLits to avoid orphans. Thanks for your input
>> though, this is exactly the kind of feedback we were hoping for :-)
>>
>> Cheers,
>>
>>     Gabor
>>
>>
>> [looks like I lost a previous version of this response, sorry if you
>> get it twice]
>>
>> On 2/7/13, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote:
>> > Hey Gabor,
>> >
>> > And why should it be part of base? Don't get me wrong, I'm not saying
>> > this
>> > is not important/useful. I'm just wondering about the reason to have it
>> > in
>> > base.
>> > Is it tied to TypeLits?
>> >
>> >
>> > Cheers,
>> > Pedro
>> >
>> > On Thu, Feb 7, 2013 at 2:21 PM, Gabor Greif <ggreif at gmail.com> wrote:
>> >
>> >> Oi Jos?,
>> >>
>> >> this is a library-only issue, the branch is in libraries/base, thus
>> >> somewhat tied to the 7.8 release.
>> >>
>> >> Cheers,
>> >>
>> >>     Gabor
>> >>
>> >> On 2/7/13, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote:
>> >> > On Wed, Feb 6, 2013 at 7:17 PM, Gabor Greif <ggreif at gmail.com>
>> >> > wrote:
>> >> >
>> >> >> On 2/6/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>> >> >> > 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).
>> >> >>
>> >> >
>> >> > Can you perhaps summarise exactly what needs to be added to GHC for
>> >> > this
>> >> to
>> >> > work?
>> >> > It's not immediately clear to me why this is not just a library
>> >> > issue.
>> >> >
>> >> >
>> >> > Thanks,
>> >> > Pedro
>> >> >
>> >>
>> >
>>
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://www.haskell.org/mailman/listinfo/ghc-devs
>>
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://www.haskell.org/mailman/listinfo/ghc-devs
>
>


Reply | Threaded
Open this post in threaded view
|

RFC: Singleton equality witnesses

Simon Peyton Jones
In reply to this post by Iavor Diatchki
Thanks for pushing on this!   The summary of my comments is this:  I think that we should have 1 or 2 low-level (not necessarily safe) GHC modules that contain all the bits that GHC needs to know about, and move all other bits into a separate library, which is to be used by the actual users of the system.  In this way, this library could evolve independently of GHC releases.

That makes sense to me.  Perhaps the bits that *are* in GHC.XX can be commented to say *why* they are?  Eg SingI needs to be there because GHC know about the singleton instances for type level literals. etc.

Simon

From: Iavor Diatchki [mailto:iavor.diatchki at gmail.com]
Sent: 12 February 2013 22:49
To: Simon Peyton-Jones
Cc: Richard Eisenberg; Jos? Pedro Magalh?es; ghc-devs
Subject: Re: RFC: Singleton equality witnesses

Hi Richard,

Thanks for pushing on this!   The summary of my comments is this:  I think that we should have 1 or 2 low-level (not necessarily safe) GHC modules that contain all the bits that GHC needs to know about, and move all other bits into a separate library, which is to be used by the actual users of the system.  In this way, this library could evolve independently of GHC releases.

Here are some more detailed comments:

On Mon, Feb 11, 2013 at 6:40 PM, Richard Eisenberg <eir at cis.upenn.edu<mailto:eir at cis.upenn.edu>> wrote:
I've just pushed a commit to the type-reasoning branch with a strawman proposal of a reorganization of these definitions. Specifically, this commit breaks TypeLits into the following five files:

- GHC.TypeEq, which contains the definitions for (:~:), Void, Refuted, etc.
- GHC.Singletons, which contains the definitions about singletons in general, such as SingI and SingEquality
- GHC.TypeLits.Unsafe, which contains just unsafeSingNat and unsafeSingSymbol
- GHC.TypeLits.Internals, which is necessary to get GHC.TypeLits.Unsafe to have access to the right internals;
this module is not exported from the 'base' package
and
- GHC.TypeLits, which contains the definitions specific to type-level literals.

Like Simon, I think that there is no need to distinguish between TypeList.Unsafe and TypeLits.Internals.

Some thoughts on this design:
- First off, why is TypeEq part of GHC?? Because we wish to write eqSingNat and eqSingSym in GHC.TypeLits, and that module rightly deserves to be part of GHC. I'm quite uncomfortable with this decision, and I even created a new git repo at github.com/goldfirere/type-reasoning<http://github.com/goldfirere/type-reasoning> to hold the definitions that eventually ended up in GHC.TypeEq. (The repo has nothing in it, now.) Perhaps the best resolution is to move eqSingNat and eqSingSym out of GHC.TypeLits and into an external package, but that seems silly in a different direction. (It is fully technically feasible, as those functions don't depend on any internals.) I would love some feedback here.

We could move these out of GHC: they are just defined using (a safe use of) `unsafeCoerce`.  They just need to know about the equality type (:~:), so I think they should be defined wherever the equality type is defined.

Also, an unrelated piece of advice:  try to keep down the use of type synonyms---they make libraries seem complex.  For example, most programmers would understand the type 'a -> Void', but when I see `Refuted a` I have to go lookup its definition and check if there is something special about it.

- Why is Singletons broken off? No strong reason here, but it seemed that the singletons-oriented definitions weren't solely related to type-level literals, so it seemed more natural this way.

I don't think this matters too much either way, but I would look for things to remove from here and move to the programmer facing library.  For example, why should `SingEquality` be there?  It is important for `SingI` to be in GHC, because the instances for type-level literals are wired into GHC: it expects the class to be in GHC.TypeLits (this is why moving the class broke the instances, take a look in `compiler/prelude/TysWiredIn.lhs`, indeed, `Nat` and `Symbol` are also wired into GHC in the same module).

- Making the Unsafe module was a little more principled, because those functions really are unsafe! They are quite useful, though, and should be available somewhere.

Yes, I think that we want to export these at least for the use by the programmer facing library---it may choose not to re-export them.

-Iavor


On Tue, Feb 12, 2013 at 12:38 AM, Simon Peyton-Jones <simonpj at microsoft.com<mailto:simonpj at microsoft.com>> wrote:
- Currently, the internals of GHC assign types like "0" the kind GHC.TypeLits.Nat, so Nat and Symbol *must* remain in the GHC.TypeLits module. Unfortunately, the plumbing around GHC.TypeLits.Unsafe want Nat and Symbol to be defined in GHC.TypeLits.Internals. So, I created a TypeLits.hs-boot file to fix the problem. This is highly unsatisfactory, and if something like what I've done here sticks around, we should change the internals of GHC to use GHC.TypeLits.Internals.Nat, getting rid of the import cycle.

Let?s NOT have an hs-boot file here.  Instead, change PrelNames to tell GHC where Nat and Symbol are defined.  It?s ok for them to be in Internals.

I?m also unconvinced about the distinction between ?Internals? and ?Unsafe?.  To me the former connotes the latter.  Import Internals if you know what you are doing; eg that might let you break important invariants.  Import a kosher module like TypeLits if you want the Joe Programmer interface.

Simon



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130213/0af02cbb/attachment-0001.htm>