Re: Type-level generics

[Evan Laforge]

On Fri, Sep 1, 2017 at 2:23 PM, Wolfgang Jeltsch
 wrote:
> Hi!
>
> Before starting with generics support at the type level, please first
> improve the generics support at the value level. When I looked at it the
> last time, there were some apparent leftovers in the form of types or
> type parameters never used. In addition, it seems awkward that you have

I was just about to complain about this myself, since every year or so
I go fail to figure out GHC.Generics after tripping over lots of out
of date documentation, confusing type aliases, and obsolete aliases,
and wrong examples, but I just looked again and it seems like
GHC.Generics got a major update in ghc 8.  It looks like there's still
one confusing reference to Par0: "Note how Par0 and Rec0 both being
mapped to K1 allows us to define a uniform instance here. " but at
least it's not tangled up in the already very confusing examples and
signatures.  I think that sentence can be deleted entirely now?  I
have no idea what it's trying to express.

So thanks to whoever did that.  I'll give it another try.
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Type-level generics

[Wolfgang Jeltsch]

Hi!

Before starting with generics support at the type level, please first
improve the generics support at the value level. When I looked at it the
last time, there were some apparent leftovers in the form of types or
type parameters never used. In addition, it seems awkward that you have
to pass these p-parameters around when working with types of kind *, and
that there is no possibility to work with types with more than one
parameter. I think that GHC’s approach to generics is very good in
general, but that the GHC.Generics module looks a bit unpolished and ad-
hoc at the moment. Maybe it would be possible to solve the
abovementioned problems using TypeInType.

All the best,
Wolfgang

Am Donnerstag, den 31.08.2017, 15:37 -0400 schrieb David Feuer:
> I've been thinking for several weeks that it might be useful to offer
> type-level generics. That is, along with
> 
> to :: Rep a k -> a
> from :: a -> Rep a
> 
> perhaps we should also derive
> 
> type family To (r :: Rep a x) :: a
> type family From (v :: a) :: Rep a x
> 
> This would allow us to use generic programming at the type level
> For example, we could write a generic ordering family:
> 
> class OrdK (k :: Type) where
>   type Compare (x :: k) (y :: k) :: Ordering
>   type Compare (x :: k) (y :: k) = GenComp (Rep k ()) (From x) (From
> y)
> 
> instance OrdK Nat where
>   type Compare x y = CmpNat x y
> 
> instance OrdK Symbol where
>   type Compare x y = CmpSymbol x y
> 
> instance OrdK [a] -- No implementation needed!
> 
> type family GenComp k (x :: k) (y :: k) :: Ordering where
>   GenComp (M1 i c f p) ('M1 x) ('M1 y) = GenComp (f p) x y
>   GenComp (K1 i c p) ('K1 x) ('K1 y) = Compare x y
>   GenComp ((x :+: y) p) ('L1 m) ('L1 n) = GenComp (x p) m n
>   GenComp ((x :+: y) p) ('R1 m) ('R1 n) = GenComp (y p) m n
>   GenComp ((x :+: y) p) ('L1 _) ('R1 _) = 'LT
>   GenComp ((x :+: y) p) ('R1 _) ('L1 _) = 'GT
>   GenComp ((x :*: y) p) (x1 ':*: y1) (x2 ':*: y2) =
> PComp (GenComp (x p) x1 x2) (y p) y1 y2
>   GenComp (U1 p) _ _ = 'EQ
>   GenComp (V1 p) _ _ = 'EQ
> 
> type family PComp (c :: Ordering) k (x :: k) (y :: k) :: Ordering
> where
>   PComp 'EQ k x y = GenComp k x y
>   PComp x _ _ _ = x
> 
> For people who want to play around with the idea, here are the
> definitions of To and From
> for lists:
> 
>   To ('M1 ('L1 ('M1 'U1))) = '[]
>   To ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs) = x ': xs
>   From '[] = 'M1 ('L1 ('M1 'U1))
>   From (x ': xs) = 'M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs
> 
> David
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: [broken HEAD] In which the strict state monad fails at basic arithmetic

[Simon Peyton Jones via ghc-devs]

Wow -- Fast work!   Do add a test case

Simon

| -Original Message-
| From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Ben
| Gamari
| Sent: 01 September 2017 14:53
| To: Moritz Angermann ; GHC developers 
| Subject: Re: [broken HEAD] In which the strict state monad fails at basic
| arithmetic
| 
| Moritz Angermann  writes:
| 
| > Hi *,
| >
| > while working on some related code.  I came across a rather peculiar
| > behavior with GHC built from the current master branch at b2c2e3e8.
| >
| The issue was a bug indeed introduced by the commit you cite below. The
| problem was a mistake in a change in constant folding which,
| frighteningly, the testsuite did not catch. See D3904 for a fix and a
| test is forthcoming.
| 
| Cheers,
| 
| - Ben

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Convenient URL alias for Trac tickets

[Ben Gamari]

Herbert Valerio Riedel  writes:

> Good idea!
>
> ...btw, note that a couple years ago, I set up the little known
>
> http://ghc.haskell.org/ticket/1234
>
> alias... :-)
>
Indeed I noticed that and it almost deterred me from adding the new
alias. However, I am sympathetic to mobile users who complain about long
urls.

Cheers,

- Ben



signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Convenient URL alias for Trac tickets

[Herbert Valerio Riedel]

Good idea!

...btw, note that a couple years ago, I set up the little known

http://ghc.haskell.org/ticket/1234

alias... :-)

On Fri, Sep 1, 2017 at 8:26 PM, Ben Gamari  wrote:
> Hello everyone,
>
> Earlier today a contributor requested that we have an easier-to-remember URL
> for Trac tickets. Consequently, I've configured ghc.haskell.org to redirect
> URLs of the form,
>
> http://ghc.haskell.org/t/$n
>
> to the appropriate Trac ticket. For instance,
> https://ghc.haskell.org/t/14171 will bring you to the ticket for #14171.
> Hopefully others also will find this helpful.
>
> Cheers,
>
> - Ben
>
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Convenient URL alias for Trac tickets

[Ben Gamari]

Hello everyone,

Earlier today a contributor requested that we have an easier-to-remember URL
for Trac tickets. Consequently, I've configured ghc.haskell.org to redirect
URLs of the form,

http://ghc.haskell.org/t/$n

to the appropriate Trac ticket. For instance,
https://ghc.haskell.org/t/14171 will bring you to the ticket for #14171.
Hopefully others also will find this helpful.

Cheers,

- Ben


signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: [broken HEAD] In which the strict state monad fails at basic arithmetic

[Ben Gamari]

Moritz Angermann  writes:

> Hi *,
>
> while working on some related code.  I came across a rather peculiar behavior
> with GHC built from the current master branch at b2c2e3e8.
>
The issue was a bug indeed introduced by the commit you cite below. The
problem was a mistake in a change in constant folding which,
frighteningly, the testsuite did not catch. See D3904 for a fix and a
test is forthcoming.

Cheers,

- Ben



signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: [broken HEAD] In which the strict state monad fails at basic arithmetic

[Ben Gamari]

Moritz Angermann  writes:

> Hi *,
>
> while working on some related code.  I came across a rather peculiar behavior
> with GHC built from the current master branch at b2c2e3e8.
>
Indeed this sounds like a real bug. Can you open a ticket?

Also, it looks like the gist has projected out directory structure; do
you think you could push the testcase as a proper git repository?

>
> PS: can we have a folder in ghc, which contains cabal packages,
> and part of the validation is just iterating over all those
> packages with `cabal new-test -w /path/to/inplace/bin/ghc-stage2`?
> In that case, one could simply change the executable target in
> [1] into a testsuite, and drop the package into that folder?
>
The problem is that we don't have access to cabal-install. However,
I think there is certainly room for this sort of testing as part of, for
instance, the nightly test cycle. In this case we'd likely want to
contain this infrastructure in a repository outside of ghc proper.

Cheers,

- Ben



signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Type-level generics

[Ryan Scott]

While we're on the topic, I'll mention that at one point I attempted
to modify the singletons [1] library so that it would automatically
generate promoted (i.e., type-level) and singled versions of Generic
instances for any data type that derived Generic. I wasn't successful,
since it turns out singletons are difficult to adapt to data types
with higher-kinded types [2] and type classes with associated type
families [3], but I did manage to write some examples on a very
limited subset of GHC.Generics in this gist [4].

The promoted version of Generic (PGeneric) in that gist works pretty
much identically to Oleg's version, but with one notable difference: I
don't attempt to put the Generic laws as a superclass of PGeneric.
Instead, I make the laws class methods of the singled version of
Generic (SGeneric). I found it more convenient to do it this way since
I needed to pattern-match on these proofs directly in a generic
implementation of decidable equality, but I'm sure this isn't the only
way it could be done.

Speaking of which, it astounds me that the Generic laws aren't
documented in the Haddocks! We really should do that.

Ryan S.
-
[1] http://hackage.haskell.org/package/singletons
[2] See the extended discussion in
https://github.com/goldfirere/singletons/issues/150
[3] https://github.com/goldfirere/singletons/issues/198
[4] https://gist.github.com/RyanGlScott/daeb63be7885244d9882dcbb1bbc10cc
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

[broken HEAD] In which the strict state monad fails at basic arithmetic

[Moritz Angermann]

Hi *,

while working on some related code.  I came across a rather peculiar behavior
with GHC built from the current master branch at b2c2e3e8.

After condensing the application quite a bit[1], the test case now produces

   8 with ghc 8.2.1 and
  -6 with ghc 8.3 @ b2c2e3e8

The sample application is essentially a strict `State Int a` monad, that is 
being 
advanced by 1 and then by another 7.

```
module Lib where

import Control.Monad.Trans.State.Strict

eval :: Int -> State Int a -> a
eval p = fst . flip runState p

advance :: Int -> State Int ()
advance = modify' . (+)

loc :: State Int Int
loc = get

emit1 :: State Int ()
emit1 = advance 1

emitN :: Int -> State Int ()
-- adding in the 0 case, breaks with HEAD. 8.2.1 is fine with it.
-- emitN 0 = advance 0
emitN 0 = pure ()
emitN n = advance n

align8 :: State Int ()
align8 = do
  bits <- (`mod` 8) <$> loc
  emitN (8 - bits)
```

with the test driver

```

module Main where

import Lib
import System.Exit

main :: IO ()
main = do
  let p = eval 0 (emit1 >> align8 >> loc)
  putStrLn $ show p
  if p == 8
then putStrLn "OK" >> exitSuccess
else putStrLn "FAIL" >> exitFailure
```

Compiling both with ghc, will *NOT* exhibit the issue. Only when the `Lib` 
module
is packed, and `Main` is linked against the package is the issue visible. A 
cabal file for this is contained in [1].

Using the following git bisect script (where [1] is in `../break` relative to 
ghc)

```
#!/bin/bash
git submodule update --init --recursive
make -s clean
make -s distclean
./boot > /dev/null

if  ./configure --silent --disable-large-address-space &&
make -s -j9
then
(cd ../break &&
 rm -fR dist-newstyle &&
 cabal new-run test -w ../ghc/inplace/bin/ghc-stage2)
status=$?
else
status=125
fi

exit $status
```

$ git bisect $PWD/bisect.sh

yields:

```
193664d42dbceadaa1e4689dfa17ff1cf5a405a0 is the first bad commit
commit 193664d42dbceadaa1e4689dfa17ff1cf5a405a0
Author: Simon Peyton Jones 
Date:   Wed Mar 8 10:26:47 2017 +

Re-engineer caseRules to add tagToEnum/dataToTag

See Note [Scrutinee Constant Folding] in SimplUtils

* Add cases for tagToEnum and dataToTag. This is the main new
  bit.  It allows the simplifier to remove the pervasive uses
  of case tagToEnum (a > b) of
False -> e1
True  -> e2
  and replace it by the simpler
 case a > b of
DEFAULT -> e1
1#  -> e2
  See Note [caseRules for tagToEnum]
  and Note [caseRules for dataToTag] in PrelRules.

* This required some changes to the API of caseRules, and hence
  to code in SimplUtils.  See Note [Scrutinee Constant Folding]
  in SimplUtils.

* Avoid duplication of work in the (unusual) case of
 case BIG + 3# of b
   DEFAULT -> e1
   6#  -> e2

  Previously we got
 case BIG of
   DEFAULT -> let b = BIG + 3# in e1
   3#  -> let b = 6#   in e2

  Now we get
 case BIG of b#
   DEFAULT -> let b = b' + 3# in e1
   3#  -> let b = 6#  in e2

* Avoid duplicated code in caseRules

A knock-on refactoring:

* Move Note [Word/Int underflow/overflow] to Literal, as
  documentation to accompany mkMachIntWrap etc; and get
  rid of PrelRuls.intResult' in favour of mkMachIntWrap
```

I do not yet understand exactly where this goes wrong. But I hope
someone else will be able to help out? I do find it curious though
that this bug seems to have gone unnoticed (assuming the commit
git bisect found is indeed the underlying issue) for almost half
a year. And please, if my analysis is faulty at some point don’t
hesitate to point that out!

Cheers,
 Moritz

PS: can we have a folder in ghc, which contains cabal packages,
and part of the validation is just iterating over all those
packages with `cabal new-test -w /path/to/inplace/bin/ghc-stage2`?
In that case, one could simply change the executable target in
[1] into a testsuite, and drop the package into that folder?

—
[1]: https://gist.github.com/angerman/c6ee51e4892ce6efdbcabb8c5ab990fa
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Type-level generics

[Oleg Grenrus]

Seems that by making a class you can "prove" by requiring this isomorphism:

class (To r ~ v, From v ~ r) -- , To (From v :: Rep a x) ~ v)
=> TypeGeneric a (r :: Rep a x) (v :: a)
  where
type To r :: a
type From v :: Rep a x

See attachment or [1] for the whole file.

Cheers, Oleg

[1]: https://gist.github.com/phadej/fab7c627efbca5cba16ba258c8f10337

On 31.08.2017 23:22, David Feuer wrote:
> One other thing I should add. We'd really, really like to have isomorphism
> evidence:
>
>   toThenFrom :: pr p -> To (From x :: Rep a p) :~: (x :: a)
>   fromThenTo :: pr1 a -> pr2 (r :: Rep a p) -> From (To r :: a) :~: (r :: Rep 
> a p)
>
> I believe these would make the To and From families considerably more
> useful. Unfortunately, while I'm pretty sure those are completely legit for
> any Generic-derived types, I don't think there's ever any way to prove
> them in Haskell! Ugh.
>
> On Thursday, August 31, 2017 3:37:15 PM EDT David Feuer wrote:
>> I've been thinking for several weeks that it might be useful to offer
>> type-level generics. That is, along with
>>
>> to :: Rep a k -> a
>> from :: a -> Rep a
>>
>> perhaps we should also derive
>>
>> type family To (r :: Rep a x) :: a
>> type family From (v :: a) :: Rep a x
>>
>> This would allow us to use generic programming at the type level
>> For example, we could write a generic ordering family:
>>
>> class OrdK (k :: Type) where
>>   type Compare (x :: k) (y :: k) :: Ordering
>>   type Compare (x :: k) (y :: k) = GenComp (Rep k ()) (From x) (From y)
>>
>> instance OrdK Nat where
>>   type Compare x y = CmpNat x y
>>
>> instance OrdK Symbol where
>>   type Compare x y = CmpSymbol x y
>>
>> instance OrdK [a] -- No implementation needed!
>>
>> type family GenComp k (x :: k) (y :: k) :: Ordering where
>>   GenComp (M1 i c f p) ('M1 x) ('M1 y) = GenComp (f p) x y
>>   GenComp (K1 i c p) ('K1 x) ('K1 y) = Compare x y
>>   GenComp ((x :+: y) p) ('L1 m) ('L1 n) = GenComp (x p) m n
>>   GenComp ((x :+: y) p) ('R1 m) ('R1 n) = GenComp (y p) m n
>>   GenComp ((x :+: y) p) ('L1 _) ('R1 _) = 'LT
>>   GenComp ((x :+: y) p) ('R1 _) ('L1 _) = 'GT
>>   GenComp ((x :*: y) p) (x1 ':*: y1) (x2 ':*: y2) =
>> PComp (GenComp (x p) x1 x2) (y p) y1 y2
>>   GenComp (U1 p) _ _ = 'EQ
>>   GenComp (V1 p) _ _ = 'EQ
>>
>> type family PComp (c :: Ordering) k (x :: k) (y :: k) :: Ordering where
>>   PComp 'EQ k x y = GenComp k x y
>>   PComp x _ _ _ = x
>>
>> For people who want to play around with the idea, here are the definitions 
>> of To and From
>> for lists:
>>
>>   To ('M1 ('L1 ('M1 'U1))) = '[]
>>   To ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs) = x ': xs
>>   From '[] = 'M1 ('L1 ('M1 'U1))
>>   From (x ': xs) = 'M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs
>>
>> David
>
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
import Data.Kind
import Data.Type.Equality
import GHC.Generics
import GHC.TypeLits

---
-- Class
---

class (To r ~ v, From v ~ r) -- , To (From v :: Rep a x) ~ v)
=> TypeGeneric a (r :: Rep a x) (v :: a)
  where
type To r :: a
type From v :: Rep a x

---
-- Iso
---

toThenFrom
:: forall a x (r :: Rep a x) (v :: a) pr. TypeGeneric a r v
=> pr x
-> To (From v :: Rep a x) :~: (v :: a)
toThenFrom _ = Refl

fromThenTo
:: forall a x (r :: Rep a x) (v :: a) pr1 pr2. TypeGeneric a r v
=> pr1 a -> pr2 (r :: Rep a x)
-> From (To r :: a) :~: (r :: Rep a x)
fromThenTo _ _ = Refl

---
-- List
---

instance TypeGeneric [k] ('M1 ('L1 ('M1 'U1))) '[] where
type To ('M1 ('L1 ('M1 'U1))) = '[]
type From '[] = 'M1 ('L1 ('M1 'U1))

instance TypeGeneric [k] ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs) (x ': xs) where
type To ('M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs) = x ': xs
type From (x ': xs) = 'M1 ('R1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('K1 xs

---
-- OrdK
---

class OrdK (k ::