Re: Explicit inequality evidence

2016-12-12 Thread Oleg Grenrus 
Hi,

I was thinking about (and almost needing) inequality evidence myself, so I’m 
:+1: to exploration.

First the bike shedding: I’d prefer /~ and :/~:.

--

new Typeable [1] would actually provide heterogenous equality:

eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)

And this one is tricky, should it be:

eqTypeRep' :: forall k1 k2 (a :: k1) (b :: k2).
   TypeRep a -> TypeRep b ->
   Either (Either (k1 :/~: k2) (a :/~: b)) (a :~~: b)

i.e. how kind inequality would work?

--

I'm not sure about propagation rules, with inequality you have to be *very* 
careful!

irreflexivity, x /~ x and symmetry x /~ y <=> y /~ x are clear.

I assume that in your rules, variables are not type families, otherwise

x /~ y => f x /~ f y doesn't hold if `f` isn't injective. (e.g. type family F x 
where F x = ())
other direction is true though.

Also:

f x ~ a -> b, is true with f ~ (->) a, x ~ b.

--

Oleg

- [1]: https://github.com/ghc-proposals/ghc-proposals/pull/16

> On 13 Dec 2016, at 06:34, David Feuer  wrote:
> 
> According to Ben Gamari's wiki page[1], the new Typeable is expected to offer
> 
> eqTypeRep :: forall k (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a 
> :~: b)
> 
> Ideally, we'd prefer to get either evidence of equality or evidence of 
> inequality. The traditional approach is to use Dec (a :~: b), where data Dec 
> a = Yes a | No (a -> Void). But  a :~: b -> Void isn't strong enough for all 
> purposes. In particular, if we want to use inequality to drive type family 
> reduction, we could be in trouble.
> 
> I'm wondering if we could expose inequality much as we expose equality. Under 
> an a # b constraint, GHC would recognize a and b as unequal. Some rules:
> 
> Base rules
> 1. f x # a -> b
> 2. If C is a constructor, then C # f x and C # a -> b
> 3. If C and D are distinct constructors, then C # D
> 
> Propagation rules
> 1. x # y <=> (x -> z) # (y -> z) <=> (z -> x) # (z -> y)
> 2. x # y <=> (x z) # (y z) <=> (z x) # (z y)
> 3. If x # y then y # x
> 
> Irreflexivity
> 1. x # x is unsatisfiable (this rule would be used for checking patterns).
> 
> With this hypothetical machinery in place, we could get something like
> 
> data a :#: b where
>   Unequal :: a # b => Unequal (a :#: b)
> 
> eqTypeRep' :: forall k (a :: k) (b :: k). TypeRep a -> TypeRep b -> Either (a 
> :#: b) (a :~: b)
> 
> Pattern matching on an Unequal constructor would reveal the inequality, 
> allowing closed type families relying on it to reduce.
> 
> Evidence structure:
> 
> Whereas (:~:) has just one value, Refl, it would be possible to imagine 
> richer evidence of inequality. If two types are unequal, then they must be 
> unequal in some particular fashion. I conjecture that we don't actually gain 
> much value by using rich evidence here. If the types are Typeable, then we 
> can explore them ourselves, using eqTypeRep' recursively to locate one or 
> more differences. If they're not, I don't think we can track the source(s) of 
> inequality in a coherent fashion. The information we got would only be 
> suitable for use in an error message. So one option would be to bundle up 
> some strings describing the known mismatch, and warn the user very sternly 
> that they shouldn't try to do anything too terribly fancy with them.
> 
> [1] https://ghc.haskell.org/trac/ghc/wiki/Typeable/BenGamari
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Explicit inequality evidence

2016-12-12 Thread David Feuer 
According to Ben Gamari's wiki page[1], the new Typeable is expected to
offer

eqTypeRep :: forall k (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a
:~: b)

Ideally, we'd prefer to get either evidence of equality or evidence of
inequality. The traditional approach is to use Dec (a :~: b), where data
Dec a = Yes a | No (a -> Void). But  a :~: b -> Void isn't strong enough
for all purposes. In particular, if we want to use inequality to drive type
family reduction, we could be in trouble.

I'm wondering if we could expose inequality much as we expose equality.
Under an a # b constraint, GHC would recognize a and b as unequal. Some
rules:

Base rules
1. f x # a -> b
2. If C is a constructor, then C # f x and C # a -> b
3. If C and D are distinct constructors, then C # D

Propagation rules
1. x # y <=> (x -> z) # (y -> z) <=> (z -> x) # (z -> y)
2. x # y <=> (x z) # (y z) <=> (z x) # (z y)
3. If x # y then y # x

Irreflexivity
1. x # x is unsatisfiable (this rule would be used for checking patterns).

With this hypothetical machinery in place, we could get something like

data a :#: b where
  Unequal :: a # b => Unequal (a :#: b)

eqTypeRep' :: forall k (a :: k) (b :: k). TypeRep a -> TypeRep b -> Either
(a :#: b) (a :~: b)

Pattern matching on an Unequal constructor would reveal the inequality,
allowing closed type families relying on it to reduce.

Evidence structure:

Whereas (:~:) has just one value, Refl, it would be possible to imagine
richer evidence of inequality. If two types are unequal, then they must be
unequal in some particular fashion. I conjecture that we don't actually
gain much value by using rich evidence here. If the types are Typeable,
then we can explore them ourselves, using eqTypeRep' recursively to locate
one or more differences. If they're not, I don't think we can track the
source(s) of inequality in a coherent fashion. The information we got would
only be suitable for use in an error message. So one option would be to
bundle up some strings describing the known mismatch, and warn the user
very sternly that they shouldn't try to do anything too terribly fancy with
them.

[1] https://ghc.haskell.org/trac/ghc/wiki/Typeable/BenGamari
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Magical function to support reflection

2016-12-12 Thread David Feuer 
On Dec 12, 2016 1:15 PM, "Edward Kmett"  wrote:

A few thoughts in no particular order:

Unlike this proposal, the existing 'reify' itself as core can actually be
made well typed.


Can you explain this?


Tagged in the example could be replaced with explicit type application if
backwards compatibility isn't a concern. OTOH, it is.


Would that help Core typing?

 On the other other hand, if you're going to be magic, you might as well go
all the way to something like:

reify# :: (p => r) -> a -> r


How would we implement reify in terms of this variant?


and admit both fundep and TF forms. I mean, if you're going to lie you
might as well lie big.


Definitely.



There are a very large number of instances out there scattered across
dozens of packages that would be broken by switching from Proxy to Tagged
or explicit type application internally. (I realize that this is a lesser
concern that can be resolved by a major version bump and some community
friction, but it does mean pragmatically that migrating to something like
this would need a plan.)


I just want to make sure that we do what we need to get Really Good Code,
if we're going to the trouble of adding compiler support.
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: [GHC] #876: Length is not a good consumer

2016-12-12 Thread Joachim Breitner 
Am Montag, den 12.12.2016, 12:44 + schrieb George Colpitts:
> my apologies, sorry for the terrible bug report

No worries! Better a bug report closed as invalid than a real bug
unreported.

Greetings,
Joachim

-- 
-- 
Joachim “nomeata” Breitner
  m...@joachim-breitner.de • https://www.joachim-breitner.de/
  XMPP: nome...@joachim-breitner.de • OpenPGP-Key: 0xF0FBF51F
  Debian Developer: nome...@debian.org

signature.asc
Description: This is a digitally signed message part
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Please don’t break travis

2016-12-12 Thread Joachim Breitner 
Hi,

taken care off, for now, it seems, see attachement.

Greetings,
Joachim
-- 
Joachim “nomeata” Breitner
  m...@joachim-breitner.de • https://www.joachim-breitner.de/
  XMPP: nome...@joachim-breitner.de • OpenPGP-Key: 0xF0FBF51F
  Debian Developer: nome...@debian.org--- Begin Message ---
-- Please reply above this line --


Hi Joachim,

Thanks for writing in! We have increased the hard build time-out to 70
minutes for the ghc/ghc repository, I hope this works for you.

We have seen that you run your builds on the container infrastructure.
You might want to try to use our `real`, sudo-enabled VMs. For some
workloads, they perform better. Have a look in our documentation to
see the differences:
https://docs.travis-ci.com/user/ci-environment/#Virtualization-environments
[1]. To try out if this brings an improvement for you, you can include
the following in the build configuration:

sudo: required
Please let us know how that works out for you.

Thanks, and have a great day!

Joep



Links:
--
[1]
https://docs.travis-ci.com/user/ci-environment/#Virtualization-environments


How would you rate my reply?
Great [1]    Okay [2]    Not Good [3]

--
Joep van Delft
Travis Builder
supp...@travis-ci.com

Visit https://www.traviscistatus.com/ [4] for service status and
uptime details
—
_Travis CI GmbH, Rigaer Str.8, 10247 Berlin, Germany | GF/CEO: Mathias
Meyer, Joshua Kalderimis | Contact: cont...@travis-ci.org |
Amtsgericht Charlottenburg, Berlin, HRB 140133 B | Umsatzsteuer-ID
gemäß §27 a Umsatzsteuergesetz: DE282002648_



Links:
--
[1]
https://secure.helpscout.net/satisfaction/105464527/record/775929667/1/
[2]
https://secure.helpscout.net/satisfaction/105464527/record/775929667/2/
[3]
https://secure.helpscout.net/satisfaction/105464527/record/775929667/3/
[4] https://www.traviscistatus.com/



> On Fri, Dec 9, 2016 at 21:17:30 UTC, Joachim Breitner 
> m...@joachim-breitner.de wrote:
> 
> Dear Travis Admins,
> 
> the main Haskell compiler, GHC, is using Travis-CI as part of its QA
> infrastructure. GHC is a large and old free software project (>20
> years), with an extensive test suite. Furthermore, as a compiler, it
> has to be compiled twice for a proper bootstrapping procedure.
> Therefore, despite leaving out a few aspects of a full validation
> build
> (which is a shame) we are have trouble getting the job to finish
> reliably in the 50 minute time frame.
> 
> I was advised on twitter¹ to write you to ask if the maximum job
> length
> limit could be increased for the ghc project (the ghc/ghc repository
> to
> be precise).
> 
> Thanks,
> Joachim
> 
> ¹ https://twitter.com/travisci/status/807315030811246596 [1]
> 
> --
> Joachim “nomeata” Breitner
> m...@joachim-breitner.de [2] • https://www.joachim-breitner.de/ [3]
> XMPP: nome...@joachim-breitner.de [4] • OpenPGP-Key: 0xF0FBF51F
> Debian Developer: nome...@debian.org [5]
> 
> Links:
> --
> [1] https://twitter.com/travisci/status/807315030811246596
> [2] mailto:m...@joachim-breitner.de
> [3] https://www.joachim-breitner.de/
> [4] mailto:nome...@joachim-breitner.de
> [5] mailto:nome...@debian.org
> 
> 
> 
> 

--- End Message ---


signature.asc
Description: This is a digitally signed message part
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: [GHC] #876: Length is not a good consumer

2016-12-12 Thread George Colpitts 
my apologies, sorry for the terrible bug report

On Sun, Dec 11, 2016 at 11:05 AM GHC  wrote:

> #876: Length is not a good consumer
> -+-
> Reporter:  ariep@…   |Owner:
> Type:  bug   |   Status:  new
> Priority:  lowest|Milestone:  7.6.2
>Component:  libraries/base|  Version:  6.5
>   Resolution:| Keywords:  length
> Operating System:  Linux | Architecture:
>  |  Unknown/Multiple
>  Type of failure:  Runtime   |Test Case:
>   performance bug|  perf/should_run/T876
>   Blocked By:| Blocking:
>  Related Tickets:|  Differential Rev(s):
>Wiki Page:|
> -+-
>
> Comment (by nomeata):
>
>  This code, compiled with `-O, does fuse, and allocates nothing (or
>  constant amounts)
>  {{{#!hs
>
>  module Foo where
>  x :: Int -> Int
>  x n = length [0..(10^n)::Int]
>  }}}
>
>  {{{
>  $ ghci -fobject-code -O Foo
>  GHCi, version 7.10.3: http://www.haskell.org/ghc/  :? for help
>  [1 of 1] Compiling Foo  ( Foo.hs, Foo.o )
>  Ok, modules loaded: Foo.
>  Prelude Foo> :set +s
>  Prelude Foo> x 1
>  11
>  (0.03 secs, 14,976,744 bytes)
>  Prelude Foo> x 7
>  1001
>  (0.02 secs, 0 bytes)
>  Prelude Foo> x 8
>  10001
>  (0.04 secs, 0 bytes)
>  }}}
>
>  (almost) HEAD:
>  {{{
>  GHCi, version 8.1.20161117: http://www.haskell.org/ghc/  :? for help
>  [1 of 1] Compiling Foo  (.hs -> .o)
>  WARNING: file compiler/simplCore/SimplCore.hs, line 663
>Simplifier bailing out after 4 iterations [58, 14, 2, 2]
>  Size = {terms: 96, types: 32, coercions: 0}
>  Ok, modules loaded: Foo (Foo.o).
>  Prelude Foo> :set +s
>  Prelude Foo> x 1
>  11
>  (0.19 secs, 94,792 bytes)
>  Prelude Foo> x 2
>  101
>  (0.01 secs, 94,648 bytes)
>  Prelude Foo> x 7
>  1001
>  (0.01 secs, 98,568 bytes)
>  Prelude Foo> x 8
>  10001
>  (0.05 secs, 98,448 bytes)
>  }}}
>
>  Testing this in with interpreted code is not sufficient, as the optimizer
>  does less in that case. So so far, everything seems as expected to me.
>
> --
> Ticket URL: 
> GHC 
> The Glasgow Haskell Compiler
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs