Re: How to implement type-level list concatenation as a GHC primitive type family

2024-08-10 Thread Iavor Diatchki
I'd say the main reason to implement `append` in GHC would be to handle
rules that can't be solved by evaluation (e.g., eliminate append [] on the
right, some associativity rule, etc.).

The speed of evaluation shouldn't really be much different as it should be
doing the same thing, more or less.

If there is a big performance hit for just straight evaluation, it might be
better to work on that part of GHC, which would also benefit other
functions, rather than adding more special cased functions.

Cheers,
Iavor

On Tue, Jul 2, 2024, 3:30 PM Hécate via ghc-devs 
wrote:

> Hi GHC devs,
>
> I was wondering recently, considering that type family evaluation is
> notoriously slow, how one would implement type-level list concatenation
> directly within GHC in a way that is much less expensive to run. So I am
> looking for pointers, as this part of GHC is fairly unknown to me.
>
> Thinking about it, I'm actually unsure where the tyfam evaluation is
> happening.
>
> Any advice would be appreciated.
>
> Cheers,
> Hécate
>
> --
> Hécate ✨
> 🐦: @TechnoEmpress
> IRC: Hecate
> WWW: https://glitchbra.in
> RUN: BSD
>
> ___
> 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: Deprecating Safe Haskell, or heavily investing in it?

2022-12-27 Thread Iavor Diatchki
Hello,

I disagree that Safe Haskell is a failed experiment, and I think with a
little work could be a very valuable tool for auditing Haskell source code.

The main change I think we should make is to completely remove the source
code annotations, and instead expose an external mechanism (e.g. some sort
of file) for specifying which potentially unsafe modules one trusts and
which modules should be safe under those assumptions.  Then GHC can do the
checking and inference just like now, and people can make their own safety
configurations depending on the threat model.

Iavor

On Tue, Dec 27, 2022, 17:08 Viktor Dukhovni  wrote:

> On Tue, Dec 27, 2022 at 09:39:22PM +0100, Hécate wrote:
>
> > I came across the nsjail system from Google a little while after posting
> > this thread: https://github.com/google/nsjail/#overview
>
> Yes, this is the sort of thing that one can begin to trust, provided
> that the exposed capabalities are managed only by inclusion, all system
> calls, filesystem namespaces, network namespaces, ... that are not
> explicitly allowed are denied.
>
> > Perhaps we could get the most value for our buck if we externalise the
> > solution to work with OS-level mechanisms?  What do you think of that?
> > Something based upon eBPF would certainly incur less modifications to
> > the RTS?
>
> Indeed, it would be simpler to leverage existing virtualisation and/or
> containerisation technologies, than build a new microkernel within the
> RTS.  Consequently, I guess I am saying that "Safe Haskell" was an
> interesting research project, but may be a practical dead-end.
>
> --
> Viktor.
> ___
> 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: Wildcards in type synonyms

2022-07-21 Thread Iavor Diatchki
Hello,

I've implemented such a feature in Cryptol, not GHC, so it is quite doable,
but I think the implementation would be easier if you decided on the
overall design of the feature first.

Some things to consider:
  * these kind of "existential" variable make sense in other type
signatures, not just type synonyms
   * there might be some contexts where you may want to disallow such
wildcards (e. g., in a data declaration)
   * you have to be careful with the scoping of type variables.  For
example, you should not unify an existential/wildcard variable with a type
that refers to variables that are not in scope of the wildcard.  I don't
remember if GHC already has a system for such things, but in Cryptol we
implanted this by having each unification variable keep track of the
quantified variables that it may depend on.

Hope this helps,
Iavor

On Fri, Jul 22, 2022, 09:30 ÉRDI Gergő  wrote:

> Hi,
>
> I'd like to implement type synonyms containing wildcards. The idea is
> that if you have `type MySyn a = MyType a _ Int`, then during
> typechecking, every occurrence of `MySyn T` would be expanded into
> `MyType T w123 Int`, with a fresh type (meta)variable `w123`.
>
> One worrying thing I noticed in my initial exploration of the GHC
> codebase is that the Core representation of `Type`s can still contain
> type synonym occurrences. And this doesn't seem like just an artefact
> of sharing the `Type` representation with `TcType`, since the
> `coreView` function also has code to look through type synonyms.
>
> What is the reason for this? I would have expected type synonyms to be
> only relevant during typechecking, and then fully resolved in the
> elaborated Core output. If that were the case, then a new version of
> `expand_syn` could live in `TcM` and take care of making these fresh
> metavariables.
>
> Beside this concrete question, taking a step back, I would also like
> to hear from people who know their way around this part of GHC, what
> they think about this and how they'd approach implementing it.
>
> Thanks,
>  Gergo
> ___
> 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: Fwd: Unlock instructions

2021-08-17 Thread Iavor Diatchki
Yeah, I got one of these too, definitely worth keeping an eye on what's
happening.

Iavor

On Mon, Aug 16, 2021, 17:16 Ben Gamari  wrote:

> Bryan Richter  writes:
>
> > Hey all,
> >
> Hi Bryan,
>
> Indeed it seems someone attempted to brute-force a few accounts but I have
> no reason to believe that they succeeded. Thanks for letting me know!
>
> 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


Re: GHC releases and versions

2021-05-28 Thread Iavor Diatchki
Hello,

I never understood what the first version number in GHC is for (the one you
refer to as "series", and that recently changed from 8 to 9).   To me it
makes more sense to have 2 numbers for proper releases and 2 numbers+date
(or git hash) for development.  So the format would be:

A.B

where A is incremented for each release (roughly 6 months apart) and B is
incremented for different variations of each release.  B resets back to 0
at each 6 month release cycle, so the very first release candidate would be
`A.0` with others being `A.1`, `A.2` etc, until the actual release seattles
at `A.R`, which would last for about 6 months when we'd go to `A+1`.  If we
need a bug fix release before the 6 month period has expired, we just bump
`B` to `A.(R+1)`, etc.

Just my 2c,
-Iavor






On Fri, May 28, 2021 at 7:49 AM Sylvain Henry  wrote:

> Hi devs,
>
> We currently have 4 branches of GHC in flight: 8.10, 9.0, 9.2 and HEAD
>
> Latest releases:
> - 8.10.4: 2021/02/06
> - 9.0.1: 2021/02/04
> - 9.2.1-alpha2: 2021/04/23
>
> Considering:
>
> 1) 8.10 branch should be stable but a lot of stuff has been merged for
> 8.10.5. To the point that 8.10.5 should probably be a "major release in
> the 8.10 series".
>
> 2) 9.0.1 is the latest major release but it shouldn't be used before
> 9.0.2 is released because of bugs and regressions (9.0.2 branch contains
> a fix for a critical bug in 9.0.1 [1] since March).
>
> 3) We might release 9.2.1 and 9.0.2 approximately at the same time which
> will be quite confusing for users ("9.0.2 in the 9.0 series and 9.2.1 in
> the 9.2 series").
>
> 4) The first major number is meaningless.
>
> Proposition:
>
> Switch to A.B.C[.D] version scheme where:
> - A: major release ("series")
> - B: major release in the A series if B>0 and C=0; beta release if B=0
> - C: bugfix release for A.B (if C>0) or beta release number (if B=0)
> - D: date when building in tree, not for releases
>
> It might be clearer exposed like this:
>
> showVersion = \case
>[a,b,c,d] -> "Dev version of " ++ showVersion [a,b,c] ++ " built on "
> ++ show d
>[a,0,c]   -> "beta " ++ show c ++ " in series " ++ show a
>[a,b,0]   -> "Major release " ++ show [a,b] ++ " in series " ++ show a
>[a,b,c]   -> "Bugfix release " ++ show c ++ " for " ++ show [a,b]
>_ -> undefined
>
>  > showVersion [9,0,1,20211028]
> "Dev version of beta 1 in series 9 built on 20211028"
>  > showVersion [9,0,1]
> "beta 1 in series 9"
>  > showVersion [9,0,2]
> "beta 2 in series 9"
>  > showVersion [9,1,0]
> "Major release [9,1] in series 9"
>  > showVersion [9,1,1]
> "Bugfix release 1 for [9,1]"
>  > showVersion [9,2,0]
> "Major release [9,2] in series 9"
>  > showVersion [10,1,0]
> "Major release [10,1] in series 10"
>
> Effects:
>
> 1) We could use C for bugfix versions which are to be released much
> faster than major versions.
> 2) B would be used for the old series we maintain. We backport a lot
> more stuff than before in older releases it seems, so it would be more
> PVP compliant to bump a major version number.
> 3) A would be used for the usual 6-month major releases.
> 4) We could make major releases in the 8 series (e.g. 8.10.5 could be
> released as 8.11.0)
> 5) We could advertise 9.0.1 as a beta (as everyone seems to consider .1
> releases)
> 6) 9.2.1 final could be released either as 9.3 (next major in the 9
> series if we just forget about 9.0.* and 9.2.*) or as 10.1.0 (first
> major in the 10 series).
> 7) No difference anymore between even/odd version numbers (for reference
> the current scheme is explained in [2])
>
> Any thoughts?
> Sylvain
>
>
> [1] https://mail.haskell.org/pipermail/haskell-cafe/2021-March/133540.html
> [2]
> https://gitlab.haskell.org/ghc/ghc/-/wikis/working-conventions/releases
>
> ___
> 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: GHC and the future of Freenode

2021-05-21 Thread Iavor Diatchki
As I said, I am not a heavy IRC user, for my online chatting needs I mostly
use Mattermost, Discord, and Slack.So I don't have an informed opinion
on the technical merits of the various platforms---mostly I've heard that
the Matrix clients and servers are quite a bit less robust than IRC ones
but I've never personally used them.

If there is a feeling that GHC wants to use a new chatting platform, by all
means we should try it out.  I just don't think that the unfortunate
situation with free-node is a good reason to drop IRC entirely.   Despite
its flows, I think it has served our community well, and while it may look
"old" to "young" users it does have the benefit of being pretty stable,
unlike the myriad of chatting services that seem to be popping up all the
time.

-Iavor



On Fri, May 21, 2021 at 10:41 AM Ben Gamari  wrote:

> Iavor Diatchki  writes:
>
> > Hello,
> >
> > I am not a heavy IRC user, but I'd say it makes most sense to just use
> > Libera.  It is essentially the same people that were running free-node
> > running pretty much the exact same service, and I believe they are trying
> > to make it extra easy to just switch, so this should be the least effort
> > transition.
> >
> > I believe IRC has served the GHC community quite well so far, and there
> is
> > a reddit post by Ed Kmett that the normal Haskell channels have already
> > been transitioned over, so I think it makes sense for GHC to stick with
> the
> > rest of the Haskell community.
> >
> The problem is that, in order to grow (or even merely not to shrink),
> the community also needs to adapt to the preferences of younger users.
>
> The fact of the matter is the younger users tend to be, at best,
> unfamiliar with IRC. In the worst case, the need to leave a browser/sign
> up for a new account means that they simply won't participate. Of the
> new contributors I have had approach me in the past year, less than half
> have had any familiarity with IRC.
>
> Matrix has the advantage of being accessible to "web-native" community
> members while being open enough to (at least in principle) allow
> community members who are accustomed to IRC to continue to participate
> via a bridge.
>
> Cheers,
>
> - Ben
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: GHC and the future of Freenode

2021-05-21 Thread Iavor Diatchki
Hello,

I am not a heavy IRC user, but I'd say it makes most sense to just use
Libera.  It is essentially the same people that were running free-node
running pretty much the exact same service, and I believe they are trying
to make it extra easy to just switch, so this should be the least effort
transition.

I believe IRC has served the GHC community quite well so far, and there is
a reddit post by Ed Kmett that the normal Haskell channels have already
been transitioned over, so I think it makes sense for GHC to stick with the
rest of the Haskell community.

-Iavor





On Fri, May 21, 2021 at 4:38 AM Moritz Angermann 
wrote:

> Fair point. From a view over the last few days, I’d say it’s closer to
> 100% on libera. Lots of people just switched. Quite surprising.
>
> On Fri, 21 May 2021 at 7:14 PM, Jens Petersen 
> wrote:
>
>> My vote goes for Matrix.
>>
>> I am not a heavy user yet, but I hope this episode helps to drive more
>> people to it away from irc.
>> Having half the people on Freenode and the other half on Libera seems the
>> worst possible outcome in the short- to mid-term.
>> The Fedora project also has plans to move to Matrix as its main group
>> chat messaging platform.
>>
>> Jens
>> ___
>> 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
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: simple Haskell help needed on #19746

2021-04-28 Thread Iavor Diatchki
Hello Richard,

Just FYI `gather` doesn't work with `readS_to_P`  (throws an error), so
you'll have to stick to ReadP parsers but, hopefully, that's OK.

-Iavor

On Tue, Apr 27, 2021 at 7:14 PM Richard Eisenberg  wrote:

>
>
> > On Apr 27, 2021, at 3:32 PM, Sebastian Graf  wrote:
> >
> > Hi Richard,
> >
> > Maybe I lack a bit of context, but I don't see why you wouldn't choose
> (3).
> > Extending the lexer/parser will yield a declarative specification of
> what exactly constitutes a GHC_OPTIONS pragma (albeit in a language that
> isn't Haskell) and should be more efficient than `reads`, even if you fix
> it to scale linearly. Plus, it seems that's what we do for other pragmas
> such as RULE already.
>
> (3) is tempting indeed. There are two problems:
>
> A. The code that parses strings isn't actually declarative. See
> https://gitlab.haskell.org/ghc/ghc/-/blob/d2399a46a01a6e46c831c19e797e656a0b8ca16d/compiler/GHC/Parser/Lexer.x#L1965.
> In particular note the comment: "This stuff is horrible. I hates it."
> Evidently written by Simon M in 2003 with the introduction of alex.
>
> B. We need this code outside the lexer, to deal with e.g. :set in GHCi.
>
> > On Apr 27, 2021, at 4:28 PM, Iavor Diatchki 
> wrote:
> >
> > ... gather ...
>
> Aha! That was the magic incantation I needed but did not have. Many
> thanks, Iavor.
>
> The curious can see
> https://gitlab.haskell.org/ghc/ghc/-/merge_requests/5509/diffs?commit_id=a560fcbbc7d4e37c4909385c55839f793b570e68#c1078a9741c11d1e15d4c678b107092790295bb3_308_317
> for the final result.
>
> Thanks!
> Richard
> ___
> 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: simple Haskell help needed on #19746

2021-04-27 Thread Iavor Diatchki
Hi Richard,

perhaps something like this would work:

```Haskell
import Text.ParserCombinators.ReadP(readP_to_S, gather)
import qualified Text.Read.Lex as L

example :: ReadS (Int,String)
example input =
  do ((xs,L.String t), rest) <- readP_to_S (gather L.lex) input
 pure ((length xs, t), rest)
```

-Iavor

On Tue, Apr 27, 2021 at 12:05 PM Richard Eisenberg  wrote:

> Hi devs,
>
> tl;dr: Is there any (efficient) way to get the String consumed by a
> `reads`?
>
> I'm stuck in thinking about a fix for #19746. Happily, the problem is
> simple enough that I could assign it in the first few weeks of a Haskell
> course... and yet I can't find a good solution! So I pose it here for
> inspiration.
>
> The high-level problem: Assign correct source spans to options within a
> OPTIONS_GHC pragma.
>
> Current approach: The payload of an OPTIONS_GHC pragma gets turned into a
> String and then processed by GHC.Utils.Misc.toArgs :: String -> Either
> String [String]. The result of toArgs is either an error string (the Left
> result) or a list of lexed options (the Right result).
>
> A little-known fact is that Haskell strings can be put in a OPTIONS_GHC
> pragma. So I can write both {-# OPTIONS_GHC -funbox-strict-fields #-} and
> {-# OPTIONS_GHC "-funbox-strict-fieds" #-}. Even stranger, I can write {-#
> OPTIONS_GHC ["-funbox-strict-fields"] #-}, where GHC will understand a list
> of strings. While I don't really understand the motivation for this last
> feature (I posted #19750 about this), the middle option, with the quotes,
> seems like it might be useful.
>
> Desired approach: change toArgs to have this type: RealSrcLoc -> String ->
> Either String [Located String], where the input RealSrcLoc is the location
> of the first character of the input String. Then, as toArgs processes the
> input, it advances the RealSrcLoc (with advanceSrcLoc), allowing us to
> create correct SrcSpans for each String.
>
> Annoying fact: Not all characters advance the source location by one
> character. Tabs and newlines don't. Perhaps some other characters don't,
> too.
>
> Central stumbling block: toArgs uses `reads` to parse strings. This makes
> great sense, because `reads` already knows how to convert Haskell String
> syntax into a proper String. The problem is that we have no idea what
> characters were consumed by `reads`. And, short of looking at the length of
> the remainder string in `reads` and comparing it to the length of the input
> string, there seems to be no way to recreate this lost information. Note
> that comparing lengths is slow, because we're dealing with Strings here.
> Once we know what was consumed by `reads`, then we can just repeatedly call
> advancedSrcLoc, and away we go.
>
> Ideas to get unblocked:
> 1. Just do the slow (quadratic in the number of options) thing, looking at
> the lengths of strings often.
> 2. Reimplement reading of strings to return both the result and the
> characters consumed
> 3. Incorporate the parsing of OPTIONS_GHC right into the lexer
>
> It boggles me that there isn't a better solution here. Do you see one?
>
> Thanks,
> Richard
> ___
> 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: How does GHC implement layout?

2021-04-04 Thread Iavor Diatchki
Hi Alexis,

I wasn't sure what the "alternative layout" is either and did some
googling, and it appears that it is something that was never really
documented properly.   The following link contains pointers to the commit
that introduced it (in 2009!)  (not the main ticket but some of the
comments)

https://ghc-tickets.haskell.narkive.com/htgwkF80/13087-alternativelayoutrule-breaks-lambdacase

Overall, I do think that Haskell's layout rule is more complicated than it
needs to be, and this is mostly because of the rule that requires the
insertion of a "virtual close curly" on a parse error.  This means that the
parser and lexer have to communicate.  I've implemented a few
languages with layout, and usually use a simpler version of layout that
just omits that case.  The benefit is that layout can be implemented as a
simple pre-processor pass on the stream of tokens,  which is much simpler
to specify and implement.   The drawback is that sometimes you have to
write programs in a slightly different way, but nothing that can't be
easily worked around.

My feeling is that it'd be pretty tricky to do layout in the parser with
grammar rules, but you may be able to do something with the parser state.
 I wonder how different it would end up looking though, as in a way that's
exactly what we are doing now, it is just that some of the state is the
lexer.

-Iavor


On Sat, Apr 3, 2021 at 5:05 PM Alexis King  wrote:

> Hi all,
>
> I’m wondering if there are any resources that discuss the design of GHC’s
> implementation of layout. (I haven’t been able to find any.) From looking
> at the code, here’s what I’ve gathered so far:
>
>- Layout is implemented in the lexer (compiler/GHC/Parser/Lexer.x).
>
>- The implementation is similar in some respects to the approach
>described in the Haskell Report, but still fairly different. Virtual braces
>and semicolons are inserted during the lexing process itself with the
>assistance of Alex lexer states (aka “start codes”).
>
>- In order to handle particularly tricky cases like
>
>if e then do x; y else z
>
>
>where the virtual close brace must be inserted in the middle of a
>line, tokens such as in and else are given special context-sensitive
>treatment. This appears to be quite subtle.
>
> Overall, I can mostly follow the code, but I still have a few unanswered
> questions:
>
>- The layout-related code consistently uses the phrase “alternative
>layout rule”—what does “alternative” mean here? Does it refer to GHC’s
>implementation of layout? Or maybe it refers to
>NondecreasingIndentation? It isn’t clear.
>
>- The implementation of layout seems quite complex, in large part
>because it has to worry about parsing concerns in the lexer in order to
>handle tricky cases like the one I provided above. Is there are reason all
>this is done in the lexer, rather than deferring some more of the work to
>the parser?
>
> I’ve found remarkably little information about implementing layout in
> general, so perhaps I’m missing some resources or keywords to search for,
> but any information or perspectives would be appreciated!
>
> Thanks,
> Alexis
> ___
> 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: Generalising KnowNat/Char/Symbol?

2021-03-16 Thread Iavor Diatchki
It's been a while since I've looked at that stuff, but your suggestion
seems reasonable to me.

On Tue, Mar 16, 2021 at 11:42 AM Sylvain Henry  wrote:

> Hi,
>
> I would like to have a KnownWord constraint to implement a type-safe
> efficient sum type. For now [1] I have:
>
> data V (vs :: [Type]) = Variant !Word Any
>
> where Word is a tag used as an index in the vs list and Any a value
> (unsafeCoerced to the appropriate type).
>
> Instead I would like to have something like:
>
> data V (vs :: [Type]) = Variant (forall w. KnownWord w => Proxy w ->
> Index w vs)
>
> Currently if I use KnownNat (instead of the proposed KnownWord), the
> code isn't very good because Natural equality is implemented using
> `naturalEq` which isn't inlined and we end up with sequences of
> comparisons instead of single case-expressions with unboxed literal
> alternatives.
>
> I could probably implement KnownWord and the required stuff (axioms and
> whatnot), but then someone will want KnownInt and so on. So would it
> instead make sense to generalise the different "Known*" we currently
> have with:
>
> class KnownValue t (v :: t) where valueSing :: SValue t v
>
> newtype SValue t (v :: t) = SValue t
>
> litVal :: KnownValue t v => proxy v -> t
>
> type KnownNat = KnownValue Natural
> type KnownChar = KnownValue Char
> type KnownSymbol = KnownValue String
> type KnownWord = KnownValue Word
>
> Thoughts?
> Sylvain
>
> [1]
>
> https://hackage.haskell.org/package/haskus-utils-variant-3.1/docs/Haskus-Utils-Variant.html
>
> ___
> 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: -ddump-json

2021-01-29 Thread Iavor Diatchki
Hello,
it seems pretty reasonable to change it, but we should change the version
number as well (well, and add it if it is not there).  In general, having a
version number is probably good practice for any outward facing machine
readable format.
-Iavor


On Fri, Jan 29, 2021 at 11:51 AM Ben Gamari  wrote:

> Richard Eisenberg  writes:
>
> > Hi devs,
> >
> > In my work with Alfredo at revising our error message infrastructure,
> > we ran across some code that renders error messages as JSON. Given
> > that our data structures are changing, it seems natural to change the
> > JSON output, too, but it's unclear whether that's wise. The manual
> > currently lists -ddump-json in the chapter on "Debugging the
> > compiler", suggesting that a change is fine, but I'm not yet
> > convinced.
> >
> I think it would be fine to change the output. However, note that there
> is a reason why this flag is in the -d flag namespace and the "Debugging
> the compiler". The output is quite unstructured and we reserve the right to
> change the representation, largely because it was hard to do better
> without first fixing #8809.
>
> After we have the new rich errors infrastucture in place I think we will
> be in a much better place to discuss a properly-supported flag (via the
> proposal process, presumably). However, I think when we do so we should
> be careful to constrain the scope of the provided output. GHC is not a
> language server and I don't think it would be wise to make it one.
>
> 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


Re: PSA: type checker plugins to be affected by upcoming changes to GHC

2020-11-19 Thread Iavor Diatchki
Hello,

I haven't worked on that stuff in Haskell for a long time, but here are
some thoughts:
  - I think plugins should generally be agnostic to the form of the
constraints they are given, thus flattening or not should not affect
them---after all, the user might have written the constraints in the
"flattened" form in the first place.  So I think a plugin needs to convert
the constraints to whatever form it assumes anyways.
  - I always thought that derived constraints were a pretty clever way for
disseminating information in the constraint solver, is there a note
somewhere on what's going to be the new mechanism?

-Iavor


On Thu, Nov 19, 2020 at 2:21 AM Christiaan Baaij 
wrote:

> I always forget what flattening did/does. Is it the thing where it turns a
> "complex" type family application:
>
> F (G y) (H z) ~ a
>
> into:
>
> G y ~ p
> H z ~ q
> F p q ~ a
>
> ?
>
> If so, then I'm all for removing that. Since I actually wrote/hacked a
> function that "reverts" that process (for [G]ivens only):
> https://hackage.haskell.org/package/ghc-tcplugins-extra-0.4/docs/src/GHC.TcPluginM.Extra.html#flattenGivens
> Which I use in all of my plugins. (PS it should perhaps be called
> "unflattenGiven"? like I said, I always get confused about flatten vs
> unflatten).
>
> On Thu, 19 Nov 2020 at 05:20, Richard Eisenberg  wrote:
>
>> Hi all,
>>
>> I'm hard at work on two significant refactorings within GHC's constraint
>> solver. The first is at
>> https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4149. It removes
>> flattening meta-variables and flattening skolems. This is a very nice
>> simplification. Instead, it just reduces type families directly. My other
>> patch (held up by the first) is at
>> https://gitlab.haskell.org/ghc/ghc/-/tree/wip/derived-refactor and will
>> remove Derived constraints, to be replaced by a little bit of cleverness in
>> suppressing certain confusing error messages. My guess is that either or
>> both of these will invalidate the current behavior of type-checker plugins.
>> Sadly, this is not just a case of finding a new function that replicates
>> the old behavior -- enough is changing under the hood that you might
>> actually have to rewrite chunks of your code.
>>
>> I have never written a type-checker plugin, and so I don't currently have
>> advice for you. But if you are a plugin author affected by this change and
>> want help, please reach out -- I would be happy to walk you through the
>> changes, and then hopefully make a little video explaining the process to
>> other plugin authors.
>>
>> Neither patch will make it for 9.0, but I expect both to be in 9.2. There
>> may be more where this came from (
>> https://gitlab.haskell.org/ghc/ghc/-/issues/18965) in the future, but
>> it's all for a good cause.
>>
>> (I have bcc'd plugin authors that I'm aware of. Just adding this in case
>> you're surprised at receiving this email.)
>>
>> Thanks,
>> Richard
>
> ___
> 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: Use of forall as a sigil

2020-11-18 Thread Iavor Diatchki
Semantically, `forall a -> a -> Int` is the same as `forall a. a -> Int`.
The two only differ in how you use them:
  * For the first one, you have to explicitly provide the type to use for
`a` at every call site, while
  * for the second one, you usually omit the type and let GHC infer it.

So overall I think it's a pretty simple idea. For me it's hard to see that
from the text in #281, but I think a lot of the complexity there
is about a fancy notation for explicitly providing the type at call sites.

-Iavor



On Wed, Nov 18, 2020 at 9:51 AM Richard Eisenberg  wrote:

> Hi Bryan,
>
> First off, sorry if my first response was a bit snippy -- it wasn't meant
> to be, and I appreciate the angle you're taking in your question. I just
> didn't understand it!
>
> This second question is easier to answer. I say "forall a arrow a arrow
> Int".
>
> But I still think there may be a deeper question here left unanswered...
>
> Richard
>
> On Nov 18, 2020, at 6:11 AM, Bryan Richter  wrote:
>
> Yeah, sorry, I think I'm in a little over my head here. :) But I think I
> can ask a more answerable question now: how does one pronounce "forall a ->
> a -> Int"?
>
> Den tis 17 nov. 2020 16:27Richard Eisenberg  skrev:
>
>> Hi Bryan,
>>
>> I don't think I understand what you're getting at here. The difference
>> between `forall b .` and `forall b ->` is only that the choice of b must be
>> made explicit. Importantly, a function of type e.g. `forall b -> b -> b`
>> can *not* pattern-match on the choice of type; it can bind a variable that
>> will be aliased to b, but it cannot pattern-match (say, against Int). Given
>> this, can you describe how `forall b ->` violates your intuition for the
>> keyword "forall"?
>>
>> Thanks!
>> Richard
>>
>> > On Nov 17, 2020, at 1:47 AM, Bryan Richter  wrote:
>> >
>> > Dear forall ghc-devs. ghc-devs,
>> >
>> > As I read through the "Visible 'forall' in types of terms"
>> > proposal[1], I stumbled over something that isn't relevant to the
>> > proposal itself, so I thought I would bring it here.
>> >
>> > Given
>> >
>> >f :: forall a. a -> a   (1)
>> >
>> > I intuitively understand the 'forall' in (1) to represent the phrase
>> > "for all". I would read (1) as "For all objects a in Hask, f is some
>> > relation from a to a."
>> >
>> > After reading the proposal, I think my intuition may be wrong, since I
>> > discovered `forall a ->`. This means something similar to, but
>> > practically different from, `forall a.`. Thus it seems like 'forall'
>> > is now simply used as a sigil to represent "here is where some special
>> > parameter goes". It could as well be an emoji.
>> >
>> > What's more, the practical difference between the two forms is *only*
>> > distinguished by ` ->` versus `.`. That's putting quite a lot of
>> > meaning into a rather small number of pixels, and further reduces any
>> > original connection to meaning that 'forall' might have had.
>> >
>> > I won't object to #281 based only on existing syntax, but I *do*
>> > object to the existing syntax. :) Is this a hopeless situation, or is
>> > there any possibility of bringing back meaning to the syntax of
>> > "dependent quantifiers"?
>> >
>> > -Bryan
>> >
>> > [1]: https://github.com/ghc-proposals/ghc-proposals/pull/281
>> > ___
>> > 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
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: !RE: Implicit reboxing of unboxed tuple in let-patterns

2020-09-10 Thread Iavor Diatchki
I am not sure what you'd expect this to do, but under what I was suggesting
it would be equivalent to
`let ~(x,y) = undefined in x `seq` y `seq ()`

Obviously it would be nice to warn/report error that this is probably a
mistake, which seems pretty easy to do.
What useful functionality do you think is lost by this?

The main tricky case I can think of is the interaction with pattern
synonyms, as one would have to keep track of
strict bindings in those.




On Thu, Sep 10, 2020 at 10:12 AM Chris Smith  wrote:

> I agree that the strictness there was surprising, but I think this may be
> a case where what is superficially expected is, in the end, inconsistent.
>
> What about:
>
> let ~(!x, !y) = undefined in ()
>
> If nested bang patterns implied strictness of their parents, this valid
> expression seems not to make any sense.  I can see a few ways to deal with
> that, but none of them seem intuitive to me.
>
> One could disallow it, and only allow strictness annotations on variables
> rather than all patterns, but this sacrifices a lot of functionality to
> avoid that surprise.  Alternatively, one could say that upward propagation
> of strictness is only a default, but that definitely feels like a hack.  It
> might make the original example behave as expected, but it is no longer for
> the expected reasons, and suddenly there is something even more complex
> going on.
>
> I don't have a strong opinion here, but I think it's important to consider
> more complex cases when making the decision.
>
> On Thu, Sep 10, 2020, 12:39 PM Iavor Diatchki 
> wrote:
>
>> Ah, yes, quite right: since the projections match the whole patterns, the
>> bang patterns in a constructor would be forced as soon as one of the fields
>> in the constructor is used, so this also diverges:
>>
>> ex3 = let (x, !y) = (5,undefined) in x
>>
>> The rule is consistent, to me it just seems quite unintuitive.
>>
>>
>>
>> On Thu, Sep 10, 2020 at 9:18 AM Richard Eisenberg 
>> wrote:
>>
>>> This whole area is clearly somewhat troublesome:
>>>
>>> On Sep 10, 2020, at 12:05 PM, Iavor Diatchki 
>>> wrote:
>>>
>>> 3. nested bang patterns in pattern bindings should count as "uses" of
>>> the value and therefore should be strict.  For example if I write `let (
>>> !x, !y ) = undefined in ()`, I think this should be equivalent to `let
>>> (x,y) = undefined in x `seq` y `seq` ()`.  With the current behavior the
>>> bang patterns don't do anything, while my guess would be that most people
>>> would expect the suggested behavior instead.  As usual, we should not allow
>>> that at the top level.
>>>
>>>
>>> This isn't quite right.
>>>
>>> Consider
>>>
>>> ex0 = let ( !x, !y ) = undefined in ()
>>> ex1 = let ( !x, !y ) = (5, undefined) in x
>>> ex2 = let ( !x, y )  = (5, undefined) in x
>>>
>>>
>>> ex0 converges, because let-bindings are lazy by default.
>>> ex1 diverges, because the bang on y means that, when the patten-match
>>> happens at all, x and y are bound strictly. So bangs *do* matter in nested
>>> patterns within pattern bindings. By contrast, ex2 converges.
>>>
>>> Again, I'm not arguing in favor of the current behavior, but I want to
>>> make sure we're all as informed as possible in this debate.
>>>
>>> Richard
>>>
>> ___
>> 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: !RE: Implicit reboxing of unboxed tuple in let-patterns

2020-09-10 Thread Iavor Diatchki
Ah, yes, quite right: since the projections match the whole patterns, the
bang patterns in a constructor would be forced as soon as one of the fields
in the constructor is used, so this also diverges:

ex3 = let (x, !y) = (5,undefined) in x

The rule is consistent, to me it just seems quite unintuitive.



On Thu, Sep 10, 2020 at 9:18 AM Richard Eisenberg  wrote:

> This whole area is clearly somewhat troublesome:
>
> On Sep 10, 2020, at 12:05 PM, Iavor Diatchki 
> wrote:
>
> 3. nested bang patterns in pattern bindings should count as "uses" of the
> value and therefore should be strict.  For example if I write `let ( !x, !y
> ) = undefined in ()`, I think this should be equivalent to `let (x,y) =
> undefined in x `seq` y `seq` ()`.  With the current behavior the bang
> patterns don't do anything, while my guess would be that most people would
> expect the suggested behavior instead.  As usual, we should not allow that
> at the top level.
>
>
> This isn't quite right.
>
> Consider
>
> ex0 = let ( !x, !y ) = undefined in ()
> ex1 = let ( !x, !y ) = (5, undefined) in x
> ex2 = let ( !x, y )  = (5, undefined) in x
>
>
> ex0 converges, because let-bindings are lazy by default.
> ex1 diverges, because the bang on y means that, when the patten-match
> happens at all, x and y are bound strictly. So bangs *do* matter in nested
> patterns within pattern bindings. By contrast, ex2 converges.
>
> Again, I'm not arguing in favor of the current behavior, but I want to
> make sure we're all as informed as possible in this debate.
>
> Richard
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: !RE: Implicit reboxing of unboxed tuple in let-patterns

2020-09-10 Thread Iavor Diatchki
Hello,

there are multiple things being discussed here, which I think is leading to
some confusion, in particular:
   1. How do pattern bindings work in normal Haskell?  It is not the case
that only the outer pattern is lazy---when the patterns are matched depends
on how the bound variables are used.  I don't think we need to make changes
here.
   2. How should patterns on unlifted types work in pattern bindings, both
nested and at the top level?  This is what started this discussion
originally.
   3. How should nested bang patterns work in pattern bindings?  This came
out from Richard's examples in response to my suggestion on how (2) might
work.
   4. Should you always be able to replace `_` with an unused name without
changing the semantics, which also came from Richard's examples.

Going backward, here are my thoughts:
  4. the answer to this should be `yes`, as it would make it consistent
with how the rest of the language works.
  3. nested bang patterns in pattern bindings should count as "uses" of the
value and therefore should be strict.  For example if I write `let ( !x, !y
) = undefined in ()`, I think this should be equivalent to `let (x,y) =
undefined in x `seq` y `seq` ()`.  With the current behavior the bang
patterns don't do anything, while my guess would be that most people would
expect the suggested behavior instead.  As usual, we should not allow that
at the top level.
  2. I think that an unlifted pattern (meaning "a pattern on a value of an
unlifted type") that is only nested in other unlifted patterns should be
strict  This includes top-level bindings as a special case, as they are not
nested in anything.
* For unlifted patterns nested in lifted patterns we have a choice:
 2.1 I suggested that, for simplicity, these should also be strict,
so that you could just say "all unlifted patterns are strict".   This would
mean that the containing (lifted) value would be always forced.
 2.2 I could also see a reasonable case being made for these not
forcing the evaluation of their containing value until the unlifted value
is demanded.   Perhaps this is more consistent with how the rest of the
language works, so I'd be on board with that choice too.

I think what I am suggesting is consistent with Arnaud's choice (1), except
it goes into a bit more details on how nested patterns should work.

Hope this clarifies things a bit,
-Iavor














On Thu, Sep 10, 2020 at 2:17 AM Spiwack, Arnaud 
wrote:

> One thing that I had missed, until Simon pointed it out, is that in a let
> pat = … expression, only the outermost pattern of pat is lazy. So
>
> let (x,Just y) = (1, undefined) in x `seq` ()
>
> Diverges. (whereas let (x,~(Just y)) = (1, undefined) in x `seq` ())
> doesn’t).
>
> So, really, we are only speaking of the outermost pattern, which does
> simplify the discussion a little.
>
> I don’t think that I share Iavor’s concern. In fact, I’ve got to say that
> I personally don’t see (1) as meaning that the pattern is actually strict.
> I just see a lazy pattern which happens to be immediately forced, because
> an unlifted variable is bound. In this view, it doesn’t follow that the
> presence of some unlifted pattern deep inside a lazy pattern ought to force
> the pattern.
>
> However, if the outermost pattern is unlifted, then it’s most likely that
> it is not intended for the pattern to be lazy. From there, I see four ways
> forward:
>
>1. Make let pat = … strict if the outermost pattern is unlifted
>2. Make let pat = … emit a warning if the outermost pattern is
>unlifted, but not explicitly banged.
>3. Decide that I’m mistaken, and that the current design is fine
>4. Decide that I’m mistaken, and that Iavor’s design it best
>
> What do you think? I’ll try and make a proposal soon (unless (3) is too
> popular for a proposal to be worth it).
>
> On Tue, Sep 8, 2020 at 12:02 AM Simon Peyton Jones simo...@microsoft.com
> <http://mailto:simo...@microsoft.com> wrote:
>
> I think this is the consistent way to interpret your rule (1) that
>> unlifted bindings are always strict
>>
>>
>>
>> But that’s not what rule (1) says.  It says that *a pattern binding is
>> strict iff it binds a variable of unlifted type*.
>>
>>
>>
>> Now I think we agree that your proposal says that *a pattern binding is
>> strict iff it or any of its sub-patterns has unlifted type, *including
>> wild-cards, variables, and constructor patterns; in fact *any*
>> sub-pattern.   Call that (2).
>>
>>
>>
>> So
>>
>>- (1) is *necessary*.
>>- (2) is strictly stronger, and will make fewer program defined.  But
>>is perhaps less surprising.
>>
>>
>>
>> I think you 

Re: !RE: Implicit reboxing of unboxed tuple in let-patterns

2020-09-07 Thread Iavor Diatchki
On Mon, Sep 7, 2020 at 5:12 AM Simon Peyton Jones via ghc-devs <
ghc-devs@haskell.org> wrote:

>
>
>
>1. I don’t understand the details of Iavor’s proposal to add that
>“unlifted patterns are strict”, in addition to (1).  Do you mean “any
>sub-pattern of the LHS has an unlifted type”? I think this is fully
>compatible with unlifted user defined data
>
> Just (# a,b #) = e
>
> would be strict.   And even
>
> MkT _ = e
>
> would be strict if   data T = MkT (# Int,Int #)
>
>
>

Yes, the first one would be strict up to the tuple, and the second one
would also be strict.  I think this is the consistent way to interpret your
rule (1) that unlifted bindings are always strict, and it shouldn't really
matter if you used a variable pattern, or a wild card pattern.  I don't
think there's any other part of the language where replacing a `_` with an
unused name changes the semantics of the program, and I don't think it
should in this case either.

Just to be fully explicit, the thing I find odd with GHC's current behavior
is that these two are different:

let MkT x = undefined in ()   --> undefined
let MkT _ = undefined in ()   --> ()

Even more explicitly:
let (_ :: Int#) = undefined in ()   --> ()-- the value `undefined` is
not representable in type `Int#` but GHC is happy to proceed because it
doesn't need to represent it
let (x :: Int#) = undefined in ()--> ()   -- same situation, but now
GHC is strict, even though it still doesn't need to represent the value.

I think that the consistent behavior is for all of these to diverge,
because laziness does not mix with unlfited values, at least in the
presence of non-termination.

-Iavor










>
>
> *From:* ghc-devs  *On Behalf Of *Richard
> Eisenberg
> *Sent:* 02 September 2020 14:47
> *To:* Spiwack, Arnaud 
> *Cc:* GHC developers 
> *Subject:* Re: Implicit reboxing of unboxed tuple in let-patterns
>
>
>
>
>
>
>
> On Sep 2, 2020, at 9:39 AM, Spiwack, Arnaud 
> wrote:
>
>
>
> Ooh… pattern synonyms for unboxed tuple. I must confess that I don't know
> what the semantics of these ought to be. It does look like an interesting
> can of worms. How do they currently desugar?
>
>
>
> Right now, there is one rule: if the type of any variable bound in the
> pattern is unlifted, then the pattern is an unlifter-var pattern and is
> strict. The pattern must be banged, unless the bound variable is not
> nested. This rule is consistent across all features.
>
>
>
> This thread is suggesting to add a special case -- one that seems to match
> intuition, but it's still a special case. And my question is: should the
> special case be for unboxed tuples? or should the special case be for any
> pattern whose overall type is unlifted?
>
>
>
> Richard
> ___
> 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: Implicit reboxing of unboxed tuple in let-patterns

2020-09-03 Thread Iavor Diatchki
Yeah, I think these are nice examples that illustrate some of the
problems with the current behavior of GHC.   For example, I think it is
weird that `b` non-terminates, but `c` does, because `z` is not used.  I
would expect those to be equivalent.

My preference would be to use the simple rule I mentioned before, but
change how bang patterns work in pattern bindings.  In particular, I think
writing a bang pattern should constitute a use of the banged value.  I
think two equivalent ways to specify this is to say that a) writing a
nested bang pattern implicitly adds bangs to the enclosing patterns, or I
think equivalently b) writing `!p` is the same as writing `x@p` and adding
`seq x` the same way we do for simple `!x = e` definitions

With this interpretation, all but `e` would diverge, which matches my
intuition of how unboxed types should work.

-Iavor


On Thu, Sep 3, 2020 at 11:02 AM Richard Eisenberg  wrote:

>
>
> On Sep 3, 2020, at 1:51 PM, Iavor Diatchki 
> wrote:
>
> How about the following rule:  unlifted patterns are always strict (i.e.,
> you desugar them as if they had an explicit  `!`).   A pattern is
> "unlifted" if the type it examines is unlifted.   Seems simple enough and,
> I think, it would do what most folks would expect.
>
>
> I don't think it's this simple. For example:
>
> > data X = MkX Int#
> >
> > a = let MkX 3# = undefined in ()
> > b = let MkX z = undefined in ()
> > c = let MkX _ = undefined in ()
> > d = let MkX {} = undefined in ()
> > e = let _ :: X = undefined in ()
>
> Which of these diverge? e definitely converges, as X is lifted. b
> definitely diverges, because it binds z, a variable of an unlifted type, to
> a component of a diverging computation.
>
> In GHC today, all the cases other than b converge.
>
> Iavor suggests that a should diverge: 3# is a pattern of an unlifted type.
> What about c? What about d? Very unclear to me.
>
> Note that banging the pattern nested inside the MkX does not change the
> behavior (in GHC today) for any of the cases where this makes sense to do
> so.
>
> Richard
>
>
> I guess a more explicit option would be to make it an error to use a lazy
> pattern on an unlifted type, and require programmers to manually add the
> `!` but I am not sure that gains much, and is more work in the compiler.
>
> -Iavor
>
> On Thu, Sep 3, 2020 at 10:38 AM Richard Eisenberg 
> wrote:
>
>>
>>
>> On Sep 3, 2020, at 12:10 PM, Spiwack, Arnaud 
>> wrote:
>>
>> This is all a tad tricky, I must say.
>>
>>
>> ... which is one of the reasons I originally wanted one simple rule. I'm
>> not now saying I was in the right, but it is an attractive resting point
>> for this discussion.
>>
>> To be clear, I don't think there's going to be any concrete action here
>> without a proposal, so perhaps once this thread finds a resting point
>> different than the status quo, someone will have to write it up.
>>
>> Richard
>> ___
>> 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: Implicit reboxing of unboxed tuple in let-patterns

2020-09-03 Thread Iavor Diatchki
How about the following rule:  unlifted patterns are always strict (i.e.,
you desugar them as if they had an explicit  `!`).   A pattern is
"unlifted" if the type it examines is unlifted.   Seems simple enough and,
I think, it would do what most folks would expect.

I guess a more explicit option would be to make it an error to use a lazy
pattern on an unlifted type, and require programmers to manually add the
`!` but I am not sure that gains much, and is more work in the compiler.

-Iavor

On Thu, Sep 3, 2020 at 10:38 AM Richard Eisenberg  wrote:

>
>
> On Sep 3, 2020, at 12:10 PM, Spiwack, Arnaud 
> wrote:
>
> This is all a tad tricky, I must say.
>
>
> ... which is one of the reasons I originally wanted one simple rule. I'm
> not now saying I was in the right, but it is an attractive resting point
> for this discussion.
>
> To be clear, I don't think there's going to be any concrete action here
> without a proposal, so perhaps once this thread finds a resting point
> different than the status quo, someone will have to write it up.
>
> Richard
> ___
> 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: RE: Hi. I'm new to this mailing list and have a few questions.

2020-08-04 Thread Iavor Diatchki
I think that's a nice idea.  In Cryptol we have both positional and named
applications (as in your outline) and it works very nicely, I think.

-Iavor

On Tue, Aug 4, 2020 at 10:46 AM Anselm Schüler (conversations subemail) <
conversat...@anselmschueler.com> wrote:

> Thank you for the nice introduction :) !
>
> I will check out the GHC proposals site.
>
> And following Simon’s (I hope addressing with first name is OK)
> suggestion, I’m going to give an outline of the idea.
>
>
>
> The idea is to extend type application syntax to enable explicit
> assignment of types to specific type variables.
>
> For instance, say I have f :: forall a b. (a, b) -> (b, a), and I want to
> apply the type [String] to it. My only option is to do
>
> f @([String]) *:: forall b. ([String], b) -> (b, [String]) *
>
> —but what if, instead, I want a function of type forall a. (a, [String])
> -> ([String], a)?
>
> I propose the following syntax:
>
> f @{b = [String]} *:: forall a. ([String], b) -> (b, [String])*
>
> This wouldn’t break any existing programs since using record syntax here
> is already disallowed and met with an error message.
>
> A question is of course the symbol used for assignment (~, =, ::, or ->?).
>
>
>
> I hope the code shows up as a monospace font on your end. I used the IBM
> Plex Mono font, which is open-source .
>
>
>
> *Anselm Schüler*
>
> *www.anselmschueler.com *
>
> *m...@anselmschueler.com *
>
>
>
> *From: *Simon Peyton Jones 
> *Sent: *Tuesday, August 4, 2020 18:44
> *To: *Richard Eisenberg ; "Anselm Schüler
> (conversations subemail)" 
> *Cc: *ghc-devs@haskell.org
> *Subject: *RE: Hi. I'm new to this mailing list and have a few questions.
>
>
>
> Welcome Anselm.  ghc-devs is a very informal mailing list, and we welcome
> newcomers.
>
>
>
> For example, I have a feature idea in the back of my mind, which I imagine
> would be easy to implement
>
>
>
> What Richard says is right, but you should feel free to fly the kite on
> this list if you want – or on Haskell Café – to get some idea of whether
> others seem warm about the idea, before writing a full proposal.
>
>
>
> Simon
>
>
>
> *From:* ghc-devs  *On Behalf Of *Richard
> Eisenberg
> *Sent:* 04 August 2020 16:05
> *To:* "Anselm Schüler (conversations subemail)" <
> conversat...@anselmschueler.com>
> *Cc:* ghc-devs@haskell.org
> *Subject:* Re: Hi. I'm new to this mailing list and have a few questions.
>
>
>
> Hi Anselm,
>
>
>
> Welcome!
>
>
>
> A good way of getting used to a list like this one is to wait a little
> while and observe what kind of messages others send; this will give you a
> feel for how the list is used. If you're impatient, you can also check out
> the archives at https://mail.haskell.org/pipermail/ghc-devs/
> 
> .
>
>
>
> As for a feature request: if your feature changes the language GHC accepts
> (most do), the right place to post is at
> https://github.com/ghc-proposals/ghc-proposals
> .
> There is a description of how to proceed on that page. Proposals submitted
> there get debated within the community and then eventually sent to a GHC
> Steering Committee for a vote on acceptance or rejection. Then, we worry
> about implementing it. If you have a suggestion that does not change the
> language GHC accepts, you can post an Issue at
> https://gitlab.haskell.org/ghc/ghc/
> 
> .
>
>
>
> I hope this is helpful!
>
> Richard
>
>
>
> On Aug 4, 2020, at 8:59 AM, Anselm Schüler (conversations subemail) <
> conversat...@anselmschueler.com> wrote:
>
>
>
> First of all, in general, I’m new to mailing lists (as used for
> discussions) in general, so a question about that:
>
> When subscribed to the mailing list, do you get *every* message, or are
> some discussions hidden?
>
>
>
> Second of all, I’d like to know what kinds of messages are appropriate
> here. I’m not familiar with coding compilers or anything of the like, so
> I’m somewhat afraid of offering unhelpful comments or being just woefully
> underqualified to participate here.
>
> For example, I have a feat

Re: How should we treat changes to the GHC API?

2020-07-27 Thread Iavor Diatchki
In principle, I think we should treat the GHC API like any other library,
and try not to break code unnecessarily.  However, my impression is that
the GHC API grew somewhat organically, so we may want to put some
additional work before we stabilize things too much.  It's been a while
since I used it, so I might be out of date, but last I looked the GHC API
was a module exporting some high-level functions from GHC.   I think that a
single module is too small of an API for a project as large as GHC.  In
fact, it probably makes sense to define more than one API.  For example,
each plugin point should probably have its own API, and that's likely
different to the GHC API that exposes functionality such as "load and type
check this module here", or "parse and evaluate this string".

-Iavor



On Mon, Jul 27, 2020 at 4:05 AM Simon Peyton Jones via ghc-devs <
ghc-devs@haskell.org> wrote:

> What I’m after is a clear opportunity for informed debate, and a clear
> yes/no decision.  That need not be high overhead.
>
>
>
> It means paying some upfront cost for design changes.  But that’s better
> than the legacy cost of dealing with things that turn out, in retrospect,
> to be less well designed than they could be.
>
>
>
> We tend to think of APIs as implementation details.  But they are deeply
> significant, and express key abstractions, just like language designs do.
> I think we should treat them just as seriously.
>
>
>
> Simon
>
>
>
> *From:* Mathieu Boespflug 
> *Sent:* 27 July 2020 11:11
> *To:* Simon Peyton Jones 
> *Cc:* ghc-devs@haskell.org Devs 
> *Subject:* Re: How should we treat changes to the GHC API?
>
>
>
> I would just point out that decision by committee, and in particular the
> GHC Proposals process, has a high cost in terms of both total human brain
> cycles and latency. The cost is entirely justified when it comes to things
> that are a) hard to revert and b) extremely hard to get right the first
> time, like new extensions to the language, or c) very sensitive (like
> governance, say). For things like breaking changes to API's, it's worth
> writing out what the current problems are. Are users complaining that the
> API churn is too high? Are they concerned about endemic quality problems
> with the API?
>
>
>
> It may be enough to make sure to know who the main users of the API are
> and tag them as reviewers on these types of changes in GitLab. Or to avoid
> extra process but enshrine principles that might be necessary to adopt,
> like saying that existing API functions should always be kept as-is during
> some deprecation period and new functionality should be exposed in new
> additions to the API. Principles to be upheld by reviewers.
>
>
>
> On Mon, Jul 27, 2020 at 10:45:50, Simon Peyton Jones 
> wrote:
>
> A recent MR for GHC
> 
> (adding machinery for plugins to write data to extensible interface files)
> made me wonder:
>
> how we should treat significant changes to the GHC API?
>
> Changes to the GHC API, especially to bits used by plugins or by IDEs, are
> clearly user-visible to an important class of users – they are not just
> internal to GHC itself.   So, how should we review them?  Should they
> perhaps be part of the GHC proposals process?  Or some other similar
> process?   (The collection of experts on the GHC API, plugins, IDEs etc, is
> rather different to the membership of the GHC steering group.)
>
> I'm asking, not to be obstructive, but because the GHC API deserves to be
> thought of as a whole; in the past it has grown incrementally, without much
> discussion, and that has not served us well.  But at the moment there is no
> process, no group to consult.
>
> Any views?
>
> Simon
>
> ___
> 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
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Error messages

2020-07-17 Thread Iavor Diatchki
It is interesting that Eric choose this particular example, as it is one of
the few types of errors where I usually find GHC's suggestions for fixes to
be quite useful---I am talking about the errors where you forgot to import
something (or you mistype it's name) and GHC suggests that you import it or
use a slightly different name.

In general, I think it's better if error messages stick to describing the
problem GHC is having, and avoid recommending solutions.   The reason I say
this is that in general we don't know what someone is trying to do and you
need that to suggest the correct fix.

In particular, often when I make a mistake it is because I have the wrong
understanding of something, be it an API or Haskell itself, and GHC can't
know what's in my head.  For example, Eric says that he imported
`QueryAnitime` but the import has `(..)` after it, which in Haskell means
import the *type* `QueryAnytime` and all its constructors, while the
problem is that we are missing a *data constructor* or pattern synonym with
that name.  Now this could be due to a typo, or maybe he doesn't know how
exactly that part of the language works, or maybe he was thinking of a
similar constructor with a slightly different name, all of which would
cause the same error but would require different fixes.

One constructive improvement to this error might be to change the words
"data constructor" to "data constructor or pattern synonym" as both of
these live in the same namespace and they are not completely interchangable
(e.g., `..` imports data constructors but not type synonyms).

Otoh, I think it'd be quite hard to suggest anything much more
sophisticated than what we already do, and for me personally, that
particular suggestion is often useful.

Iavor







On Fri, Jul 17, 2020, 02:09 Ben Gamari  wrote:

> On July 17, 2020 12:10:33 AM EDT, Erik de Castro Lopo <
> mle...@mega-nerd.com> wrote:
> >Hi all,
> >
> >Although it was many years ago I did spend soem time working on GHC
> >and I do know what a thankless task it is. I made a compliant about
> >GHC error messages on an internal Slack channel and Mortiz encouraged
> >me to repeat it here.
> >
> >I am incredibly happy about the quality of error messges for older
> >more standard parts of Haskell, probably most things in Haskell98
> >and Haskell2010.
> >
> >By way of contrast, error messages for some newer parts of Haskell are
> >incredibly poor. In fact, for the new parts, the error rmessages are
> >often wrong, just defaulting to error messages for older parts of
> >Haskell.
> >
> >As an example (open source code in a public GH repo):
> >
> >  src/Cardano/DbSync/StateQuery.hs:87:44: error:
> >  • Data constructor not in scope:
> >  QueryAnytime
> >:: QueryHardFork xs0 (Interpreter xs0)
> >   -> Query
> >(CardanoBlock TPraosStandardCrypto)
> >(Interpreter (CardanoEras TPraosStandardCrypto))
> >  • Perhaps you want to add ‘QueryAnytime’ to the import list
> >in the import of
> >‘Ouroboros.Consensus.HardFork.Combinator.Ledger.Query’
> >(src/Cardano/DbSync/StateQuery.hs:49:1-116).
> > |
> >87 |   queryHistoryInterpreter connInfo (point, QueryAnytime
> >GetInterpreter)
> >
> >The suggestion is that I need to import `QueryAnytime` but just 20 line
> >above I
> >have:
> >
> >import Ouroboros.Query (QueryAnytime (..), QueryHardFork
> >(GetInterpreter))
> >
> >The problem is that `QueryAnytime` is defined as a pattern synonym. I
> >have only
> >the tinest amount of experience using pattern synonyms and that error
> >message
> >is not really useful.
> >
>
> I am not sure that I would call this error wrong or misleading. However, I
> also suspect that it could do more to help you. GHC is claiming it is
> looking for a data constructor because that is precisely what it is looking
> for: Pattern synonyms are supposed to behave identically to data
> constructors.
>
> It sounds to me like Ouroboros.Query should be exporting the
> QueryAnytime pattern bundled with the QueryAnytime type. If this were the
> case then your import would work as you expect.
>
> In principle GHC could suggest this (e.g. in the case where a module
> exports a type `T`, separately a pattern `T`, and the user imports the
> former but not the latter). However, this is in a way a strange suggestion
> as it would be suggesting a change in a module other than the module
> currently being compiled. This could be quite confusing since it may reveal
> internal implementation details of a library that the user is not supposed
> to be exposed to.
>
> This is really more of a code style lintthan it is a compiler error.
>
> >I would like to suggest that a prerequesite for merging of new features
> >would
> >be that it provides good error messages and more importantly does not
> >provide
> >wrong or misleading error messages like the one above.
> >
> Indeed this is something that we consider during review. Howe

Re: Async exceptions and delimited continuations

2020-07-02 Thread Iavor Diatchki
Hi,

I am by no means an expert on the GHC RTS but all 3 suggestions seem quite
reasonable to me.   A good way to make a decision might be to collect some
data, at least for the things that might be easy to measure.   In
particular, it would be interesting to temporarily disable the optimization
and run some benchmarks on some IO/exceptions heavy code (some sort of
server?  or maybe a synthetic benchmark to really stress the
masking/unmaksing) and see what's the change in performance.

-Iavor









On Wed, Jul 1, 2020 at 12:13 PM Alexis King  wrote:

> Hi all,
>
> As some of you are likely aware, I have an open GHC proposal[1] to add
> native support for delimited continuations to the RTS. I also have an
> incomplete implementation,[2] and the only major remaining obstacle
> concerns async exceptions. The issue is subtle, so I’ve tried to
> provide all the necessary context in this email. If you’re already
> familiar with the ideas at play, you can skip the context about how
> delimited continuations work.
>
> For those unfamiliar, delimited continuations allow capturing slices
> of the call stack and restoring them later. For example, the program
>
> do y <- prompt $ do x <- control0 $ \k -> k (pure 10)
> pure (x + 5)
>print y
>
> will print 15. To understand what’s happening operationally, we can
> imagine an abstract call stack made up of continuation frames:
>
> ┌──┐
> │  ● + 5   │redex: control0 $ \k -> k (pure 10)
> ├──┤
> │ prompt ● │
> ├──┤
> │ print ●  │
> ├──┤
> │   ...│
> ├──┤
>
> Here, each ● represents the “hole” where the evaluated result of the
> redex will be returned. `control0` moves all the frames between the
> top of the stack and the first `prompt` into the heap and returns a
> reference to them, so after a single reduction step, we have
>
> ┌──┐
> │ print ●  │redex: k1 (pure 10)
> ├──┤heap:  k1 = ┌──┐
> │   ...││  ● + 5   │
> ├──┤└──┘
>
> When a continuation is applied, its stored stack frames are copied
> back onto the top of the current stack, and the argument becomes the
> new redex:
>
> ┌──┐
> │  ● + 5   │redex: pure 10
> ├──┤
> │ print ●  │
> ├──┤
> │   ...│
> ├──┤
>
> Now it should hopefully be clear how we end up printing 15.
>
> With that context, consider the following expression:
>
> prompt $ mask_ $ do x <- control0 $ \k -> k (pure 10)
> f x
>
> The call stack at the point of control0 looks very similar in this
> program, but now we have a use of `mask_` in there as well:
>
> ┌──┐
> │   f ●│redex: control0 $ \k -> k (pure 10)
> ├──┤exns:  masked
> │ mask_ ●  │
> ├──┤
> │ prompt ● │
> ├──┤
> │   ...│
> ├──┤
>
> When capturing the continuation, we’ll unwind the stack the same way
> we did before. Because we’re popping mask_ off the stack, we’ll unmask
> async exceptions:
>
> ┌──┐redex: k1 (pure 10)
> │   ...│exns:  not masked
> ├──┤heap:  k1 = ┌──┐
> │   f ●│
> ├──┤
> │ mask_ ●  │
> └──┘
>
> Now when we apply `k1`, we’ll copy the `mask_` frame back onto the
> stack, and we must re-mask async exceptions. Otherwise, exceptions
> will not be masked during the call to `f`, which would be wrong.
>
> Why is this a problem? The RTS applies an optimization: if you call
> mask_ (actually maskAsyncExceptions#) while exceptions are already
> masked, it doesn’t push a new stack frame at all. So, for example, if
> you write
>
> mask_ $ mask_ $ foo bar
>
> you’ll end up with only one mask_ frame on the call stack, not two.
> This tiny optimization actually allows not one but two savings:
>
> 1. The immediate benefit is that we save a stack frame.
>
> 2. The hidden benefit is that we never need to push the old
>exception masking state onto the stack.
>
>If we had multiple mask_ frames on the stack simultaneously, we
>wouldn’t know what to do when returning: should we unmask them,
>or should they stay masked? We’d need to push that information
>onto the stack in the same way we must push a return address
>when calling a function.
>
>By skipping these redundant stack frames, we can always be
>certain the right thing to do on return is to unmask async
>exceptions. No need to store anything else.
>
> (This explanation is a slight simplification, especially once
> maskUninterruptible comes into play, but it’s close enough.)
>
> Now you may see the looming problem: this strategy completely breaks
> down in the 

Re: New implementation for `ImpredicativeTypes`

2019-09-06 Thread Iavor Diatchki
Why would you infer this type as opposed to `[exists a. a]`?

On Fri, Sep 6, 2019 at 12:08 PM Vladislav Zavialov
 wrote:
>
> Iavor,
>
> Alex’s example can be well-typed if we allow first-class existentials:
>
>   [1, ‘a’, “b”] :: [exists a. Show a => a]
>
> This has nothing to do with the definition of lists. I believe the confusion 
> was between existential types and impredicative types, as Simon has pointed 
> out.
>
> - Vlad
>
> > On 6 Sep 2019, at 20:56, Iavor Diatchki  wrote:
> >
> > Hello Alex,
> >
> > the issue with your example is not the mapping of `show` but the list
> > `[1, 'a', "b"]`.  It is not well typed simply because of how lists are
> > defined.   Remember that `[1, 'a', "b"]` is not really special---it is
> > just syntactic sugar for `1 : 'a' : "b" : []` and the type of `(:)`
> > requires the elements to have the same type.
> >
> > Of course, in principle, one could define a different list type that
> > allowed values of arbitrary types to be stored in it (e.g., the
> > example list would be just of type `List`).
> > The issue is that you can't really use the elements of such a list as
> > you wouldn't know what type they have.
> >
> > Yet another option is to define a list type where the "cons" operation
> > remembers the types of the elements in the type of the constructed
> > list---at this point the lists become more like tuples (e.g., the
> > example would be of type `List [Int,Char,String]`).   This is
> > possible, but then them `map` function would have an interesting
> > type...
> >
> > I'd be happy to answer more questions but I don't want to side-track
> > the thread as all this is quite orthogonal to impredicative types.
> >
> > -Iavor
> >
> >
> >
> >
> >
> >
> >
> >
> >
> > On Fri, Sep 6, 2019 at 7:21 AM Alex Rozenshteyn  
> > wrote:
> >>
> >> Hi Simon,
> >>
> >> You're exactly right, of course. My example is confusing, so let me see if 
> >> I can clarify.
> >>
> >> What I want in the ideal is map show [1, 'a', "b"]. That is, minimal 
> >> syntactic overhead to mapping a function over multiple values of distinct 
> >> types that results in a homogeneous list. As the reddit thread points out, 
> >> there are workarounds involving TH or wrapping each element in a 
> >> constructor or using bespoke operators, but when it comes down to it, none 
> >> of them actually allows me to say what I mean; the TH one is closest, but 
> >> I reach for TH only in times of desperation.
> >>
> >> I had thought that one of the things preventing this was lack of 
> >> impredicative instantiation, but now I'm not sure. Suppose Haskell did 
> >> have existentials; would map show @(exists a. Show a => a) [1, 'a', "b"] 
> >> work in current Haskell and/or in quick-look?
> >>
> >> Tangentially, do you have a reference for what difficulties arise in 
> >> adding existentials to Haskell? I have a feeling that it would make 
> >> working with GADTs more ergonomic.
> >>
> >> On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones  
> >> wrote:
> >>>
> >>> I’m confused.   Char does not have the type (forall a. Show a =>a), so 
> >>> our example is iill-typed in System F, never mind about type inference.  
> >>> Perhaps there’s a typo?   I think you may have ment
> >>>
> >>>   exists a. Show a => a
> >>>
> >>> which doesn’t exist in Haskell.  You can write existentials with a data 
> >>> type
> >>>
> >>>
> >>>
> >>> data Showable where
> >>>
> >>>   S :: forall a. Show a => a -> Showable
> >>>
> >>>
> >>>
> >>> Then
> >>>
> >>>   map show [S 1, S ‘a’, S “b”]
> >>>
> >>> works fine today (without our new stuff), provided you say
> >>>
> >>>
> >>>
> >>>   instance Show Showable where
> >>>
> >>> show (S x) = show x
> >>>
> >>>
> >>>
> >>> Our new system can only type programs that can be written in System F.   
> >>> (The tricky bit is inferring the impredicative instantiations.)
> >>>
> >>>

Re: New implementation for `ImpredicativeTypes`

2019-09-06 Thread Iavor Diatchki
Hello Alex,

the issue with your example is not the mapping of `show` but the list
`[1, 'a', "b"]`.  It is not well typed simply because of how lists are
defined.   Remember that `[1, 'a', "b"]` is not really special---it is
just syntactic sugar for `1 : 'a' : "b" : []` and the type of `(:)`
requires the elements to have the same type.

Of course, in principle, one could define a different list type that
allowed values of arbitrary types to be stored in it (e.g., the
example list would be just of type `List`).
The issue is that you can't really use the elements of such a list as
you wouldn't know what type they have.

Yet another option is to define a list type where the "cons" operation
remembers the types of the elements in the type of the constructed
list---at this point the lists become more like tuples (e.g., the
example would be of type `List [Int,Char,String]`).   This is
possible, but then them `map` function would have an interesting
type...

I'd be happy to answer more questions but I don't want to side-track
the thread as all this is quite orthogonal to impredicative types.

-Iavor









On Fri, Sep 6, 2019 at 7:21 AM Alex Rozenshteyn  wrote:
>
> Hi Simon,
>
> You're exactly right, of course. My example is confusing, so let me see if I 
> can clarify.
>
> What I want in the ideal is map show [1, 'a', "b"]. That is, minimal 
> syntactic overhead to mapping a function over multiple values of distinct 
> types that results in a homogeneous list. As the reddit thread points out, 
> there are workarounds involving TH or wrapping each element in a constructor 
> or using bespoke operators, but when it comes down to it, none of them 
> actually allows me to say what I mean; the TH one is closest, but I reach for 
> TH only in times of desperation.
>
> I had thought that one of the things preventing this was lack of 
> impredicative instantiation, but now I'm not sure. Suppose Haskell did have 
> existentials; would map show @(exists a. Show a => a) [1, 'a', "b"] work in 
> current Haskell and/or in quick-look?
>
> Tangentially, do you have a reference for what difficulties arise in adding 
> existentials to Haskell? I have a feeling that it would make working with 
> GADTs more ergonomic.
>
> On Fri, Sep 6, 2019 at 12:33 AM Simon Peyton Jones  
> wrote:
>>
>> I’m confused.   Char does not have the type (forall a. Show a =>a), so our 
>> example is iill-typed in System F, never mind about type inference.  Perhaps 
>> there’s a typo?   I think you may have ment
>>
>>exists a. Show a => a
>>
>> which doesn’t exist in Haskell.  You can write existentials with a data type
>>
>>
>>
>> data Showable where
>>
>>S :: forall a. Show a => a -> Showable
>>
>>
>>
>> Then
>>
>>map show [S 1, S ‘a’, S “b”]
>>
>> works fine today (without our new stuff), provided you say
>>
>>
>>
>>instance Show Showable where
>>
>>  show (S x) = show x
>>
>>
>>
>> Our new system can only type programs that can be written in System F.   
>> (The tricky bit is inferring the impredicative instantiations.)
>>
>>
>>
>> Simon
>>
>>
>>
>> From: ghc-devs  On Behalf Of Alex Rozenshteyn
>> Sent: 06 September 2019 03:31
>> To: Alejandro Serrano Mena 
>> Cc: GHC developers 
>> Subject: Re: New implementation for `ImpredicativeTypes`
>>
>>
>>
>> I didn't say anything when you were requesting use cases, so I have no right 
>> to complain, but I'm still a little disappointed that this doesn't fix my 
>> (admittedly very minor) issue: 
>> https://www.reddit.com/r/haskell/comments/3am0qa/existentials_and_the_heterogenous_list_fallacy/csdwlp2/?context=8&depth=9
>>
>>
>>
>> For those who don't want to click on the reddit link: I would like to be 
>> able to write something like map show ([1, 'a', "b"] :: [forall a. Show a => 
>> a]), and have it work.
>>
>>
>>
>> On Wed, Sep 4, 2019 at 8:13 AM Alejandro Serrano Mena  
>> wrote:
>>
>> Hi all,
>>
>> As I mentioned some time ago, we have been busy working on a new 
>> implementation of `ImpredicativeTypes` for GHC. I am very thankful to 
>> everybody who back then sent us examples of impredicativity which would be 
>> nice to support, as far as we know this branch supports all of them! :)
>>
>>
>>
>> If you want to try it, at 
>> https://gitlab.haskell.org/trupill/ghc/commit/a3f95a0fe0f647702fd7225fa719a8062a4cc0a5/pipelines?ref=quick-look-build
>>  you can find the result of the pipeline, which includes builds for several 
>> platforms (click on the "Artifacts" button, the one which looks like a 
>> cloud, to get them). The code is being developed at 
>> https://gitlab.haskell.org/trupill/ghc.
>>
>>
>>
>> Any code should run *unchanged* except for some eta-expansion required for 
>> some specific usage patterns of higher-rank types. Please don't hesitate to 
>> ask any questions or clarifications about it. A merge request for tracking 
>> this can be found at https://gitlab.haskell.org/ghc/ghc/merge_requests/1659
>>
>>
>>
>> Kind rega

Re: A few questions about BuiltInSynFamily/CoAxiomRules

2019-08-27 Thread Iavor Diatchki
Hello Jan,

I think I added these sometime ago, and here is what I recall:

  * `sfInteractTop` and `sfInteractInert` are to help with type inference:
 they generate new "derived" constraints, which are used by GHC to
instantiate unification variables.
   - `sfInteractTop` is for facts you can get just by looking at a
single constraint.  For example, if we see `(x + 5) ~ 8` we can
generate a new derived constraint `x ~ 3`
   - `sfInteractIntert` is for facts that you can get by looking
at two constraints together.  For example, if we see `(x + a ~ z, x +
b ~ x)` we can generate new derived constraint `a ~ b`.
 - since "derived" constraint do not need evidence, these are just
equations.

  * `sfMatchFun` is used to evaluate built-in type families.  For
example if we see `5 + 3`, we'd like ghc to reduce this to `8`.
 - you are correct that the input list are the arguments (e.g., `[5,3]`)
 - the result is `Just` if we can perform an evaluation step, and
the 3-tuple contains:
 1. the axiom rule to be used in the evidence (e.g. "AddDef")
 2. indexes for the axiom rule (e.g.,"[5,3]")  (see below for more info)
 3. the result of evaluation (e.g., "8")

Part 2 is probably the most confusing, and I think it might have
changed a bit since I did it,
or perhaps I just forgot some of the details. Either way, this is best
explained with
an example.   The question is "What should be the evidence for `3 + 5 ~ 8`?".

In ordinary math one could do a proof by induction, but we don't
really represent
numbers in the unary notation and we don't have a way to represent inductive
proofs in GHC, so instead we decided to have an indexed family of axioms,
kind of like this:

   * AddDef(3,5)  : `(3 + 5) ~ 8`
   * AddDef(2,1) : `(2 + 1) ~ 3`
* ...

So the types in the second element of the tuple are these indexes that tell you
how to instantiate the rule.

This is the basic idea, but axioms are encoded in a slightly different
way---instead of being parameterized by just types, they  are parameterized
by equalities (the reason for this is what I seem to have forgotten,
or perhaps it changed).
So the `CoAxiomRules` actually look like this:

   * AddDef: (x ~ 3, y ~ 5) => (x + y ~ 8)

When we evaluate we always seem to be passing trivial (i.e., "refl") equalities
constructed using the second entry in the tuple.  For example, if `sfMathcFun`
returns `Just (axiom, [t1,t2], result)`, then the result will be `result`, and
the evidence that `MyFun args ~ result` will be `axiom (refl @ t1, refl @ t2)`

You can see the actual code for this if you look for `sfMatchFun` in
`types/FamInstEnv.hs`.

I hope this makes sense, but please ask away if it is unclear.  And, of course,
it would be great to document this properly.

-Iavor

















On Tue, Aug 27, 2019 at 3:57 PM Jan van Brügge  wrote:
>
> Hi lovely people,
>
> sorry if my recent emails are getting annoying.
>
> In the last few days I refactored my code to use `BuiltInSynFamily` and
> `CoAxiomRule` to replace what was very ad-hoc code. So far so easy. But
> I have a few questions due to sparse documentation.
>
> First, about `BuiltInSynFamily`. It is a record of three functions. From
> what I can tell by looking at `TcTypeNats`, the two `interact` functions
> are used to solve the argument parts of builtin families based on known
> results. `interactTop` seems to simply constraints on their own,
> `interactInert` seems to simplify based on being given two similar
> contraints.
>
> By big questions is what exactly `matchFam` does. The argument seems to
> be the arguments to the type family, but the tuple in the result is less
> clear. The axiom rule is the proof witness, the second argument I guess
> is the type arguments you actually care about? What is this used for?
> The last one should be the result type.
>
> Attached to that, what are the garantuees about the list of types that
> you get? I assumed at first they were all flattened, but my other type
> family is not. I am talking about this piece of code here:
>
> ```
> matchFamRnil :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
> matchFamRnil [] = Just (axRnilDef, [], mkRowTy k v [])
> where binders = mkTemplateKindTyConBinders [liftedTypeKind,
> liftedTypeKind]
>   [k, v] = map (mkTyVarTy . binderVar) binders
> matchFamRnil _ = Nothing
>
>
> matchFamRowExt :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
> matchFamRowExt [_k, _v, x, y, row@(RowTy (MkRowTy k v flds))] = Just
> (axRowExtDef, [x, y, row], RowTy (MkRowTy k v $ (x, y):flds))
> matchFamRowExt [k, v, x, y, _rnil] = Just (axRowExtRNilDef, [k, v],
> RowTy (MkRowTy k v [(x, y)]))
> matchFamRowExt _ = Nothing
>
> ```
>
> I needed an extra `_rnil` case  in `matchFamRowExt` because `RowExt
> "foo" Int RNil` did not match the first pattern match (the dumped list I
> got was `[Symbol, Type, "foo", Int, RNil]`). Also, is there a better way
> to conjure up polykinded variables out of the blue or is this fine? I
> tho

Re: Container type classes

2019-05-30 Thread Iavor Diatchki
Yeah, there is really no relation between the two parameters of `Fun`,
so you'd have to specify the intermediate type manually. For example:

add3 :: forall s. (Fun s s, Elem s ~ Int) => s -> s
add3 = colMap @s (+1) . colMap (+2)

I wouldn't say that it's a particularly convenient interface to work
with, unless you are working in a setting where most of the containers
have known types.


On Thu, May 30, 2019 at 2:58 PM Andrey Mokhov
 wrote:
>
> Many thanks Iavor,
>
> This looks very promising! I played with your encoding a little, but quickly 
> came across type inference issues. The following doesn't compile:
>
> add3 :: (Fun s s, Elem s ~ Int) => s -> s
> add3 = colMap (+1) . colMap (+2)
>
> I'm getting:
>
> * Could not deduce: Elem a0 ~ Int
>   from the context: (Fun s s, Elem s ~ Int)
> bound by the type signature for:
>add3 :: forall s. (Fun s s, Elem s ~ Int) => s -> s
>   Expected type: Elem a0 -> Elem s
> Actual type: Int -> Int
>   The type variable `a0' is ambiguous
>
> Fun s s is supposed to say that the intermediate type is `s` too, but I guess 
> this is not how type class resolution works.
>
> Cheers,
> Andrey
>
> -Original Message-
> From: Iavor Diatchki [mailto:iavor.diatc...@gmail.com]
> Sent: 30 May 2019 22:38
> To: Brandon Allbery 
> Cc: Andrey Mokhov ; Andreas Klebinger 
> ; ghc-devs@haskell.org
> Subject: Re: Container type classes
>
> This is how you could define `map`.  This is just for fun, and to
> discuss Haskell idioms---I am not suggesting we should do it.  Of
> course, it might be a bit more general than what you'd like---for
> example it allows defining instances like `Fun IntSet (Set Int)` that,
> perhaps?, you'd like to disallow:
>
> {-# LANGUAGE MultiParamTypeClasses, TypeFamilies #-}
>
> import Data.Set (Set)
> import qualified Data.Set as Set
> import Data.IntSet (IntSet)
> import qualified Data.IntSet as ISet
>
> class Col t where
>   type Elem t
>   -- ... As in Andreas's example
>
> class (Col a, Col b) => Fun a b where
>   colMap :: (Elem a -> Elem b) -> a -> b
>
> instance Col (Set a) where
>   type Elem (Set a) = a
>
> instance Col IntSet where
>   type Elem IntSet = Int
>
> instance Fun IntSet IntSet where
>   colMap = ISet.map
>
> instance Ord b => Fun (Set a) (Set b) where
>   colMap = Set.map
>
> On Thu, May 30, 2019 at 2:32 PM Brandon Allbery  wrote:
> >
> > They can, with more work. You want indexed monads, so you can describe 
> > types that have e.g. an ordering constraint as well as the Monad constraint.
> >
> > On Thu, May 30, 2019 at 5:26 PM Andrey Mokhov 
> >  wrote:
> >>
> >> Hi Artem,
> >>
> >>
> >>
> >> Thanks for the pointer, but this doesn’t seem to be a solution to my 
> >> challenge: they simply give up on overloading `map` for both Set and 
> >> IntSet. As a result, we can’t write polymorphic functions over Set and 
> >> IntSet if they involve any mapping.
> >>
> >>
> >>
> >> I looked at the prototype by Andreas Klebinger, and it doesn’t include the 
> >> method `setMap` either.
> >>
> >>
> >>
> >> Perhaps, Haskell’s type classes just can’t cope with this problem.
> >>
> >>
> >>
> >> *ducks for cover*
> >>
> >>
> >>
> >> Cheers,
> >>
> >> Andrey
> >>
> >>
> >>
> >> From: Artem Pelenitsyn [mailto:a.pelenit...@gmail.com]
> >> Sent: 30 May 2019 20:56
> >> To: Andrey Mokhov 
> >> Cc: ghc-devs@haskell.org; Andreas Klebinger 
> >> Subject: Re: Container type classes
> >>
> >>
> >>
> >> Hi Andrey,
> >>
> >>
> >>
> >> FWIW, mono-traversable 
> >> (http://hackage.haskell.org/package/mono-traversable) suggests decoupling 
> >> IsSet and Funtor-like.
> >>
> >>
> >>
> >> In a nutshell, they define the IsSet class (in Data.Containers) with 
> >> typical set operations like member and singleton, union and intersection. 
> >> And then they tackle a (seemingly) independent problem of mapping 
> >> monomorphic containers (like IntSet, ByteString, etc.) with a separate 
> >> class MonoFunctor (in Data.MonoTraversable):
> >>
> >>
> >>
> >> class MonoFunctor mono where
> >> omap :: (Element mono -> Element mono) -> mono -> mono
> >>
> >>
&g

Re: Container type classes

2019-05-30 Thread Iavor Diatchki
This is how you could define `map`.  This is just for fun, and to
discuss Haskell idioms---I am not suggesting we should do it.  Of
course, it might be a bit more general than what you'd like---for
example it allows defining instances like `Fun IntSet (Set Int)` that,
perhaps?, you'd like to disallow:

{-# LANGUAGE MultiParamTypeClasses, TypeFamilies #-}

import Data.Set (Set)
import qualified Data.Set as Set
import Data.IntSet (IntSet)
import qualified Data.IntSet as ISet

class Col t where
  type Elem t
  -- ... As in Andreas's example

class (Col a, Col b) => Fun a b where
  colMap :: (Elem a -> Elem b) -> a -> b

instance Col (Set a) where
  type Elem (Set a) = a

instance Col IntSet where
  type Elem IntSet = Int

instance Fun IntSet IntSet where
  colMap = ISet.map

instance Ord b => Fun (Set a) (Set b) where
  colMap = Set.map

On Thu, May 30, 2019 at 2:32 PM Brandon Allbery  wrote:
>
> They can, with more work. You want indexed monads, so you can describe types 
> that have e.g. an ordering constraint as well as the Monad constraint.
>
> On Thu, May 30, 2019 at 5:26 PM Andrey Mokhov  
> wrote:
>>
>> Hi Artem,
>>
>>
>>
>> Thanks for the pointer, but this doesn’t seem to be a solution to my 
>> challenge: they simply give up on overloading `map` for both Set and IntSet. 
>> As a result, we can’t write polymorphic functions over Set and IntSet if 
>> they involve any mapping.
>>
>>
>>
>> I looked at the prototype by Andreas Klebinger, and it doesn’t include the 
>> method `setMap` either.
>>
>>
>>
>> Perhaps, Haskell’s type classes just can’t cope with this problem.
>>
>>
>>
>> *ducks for cover*
>>
>>
>>
>> Cheers,
>>
>> Andrey
>>
>>
>>
>> From: Artem Pelenitsyn [mailto:a.pelenit...@gmail.com]
>> Sent: 30 May 2019 20:56
>> To: Andrey Mokhov 
>> Cc: ghc-devs@haskell.org; Andreas Klebinger 
>> Subject: Re: Container type classes
>>
>>
>>
>> Hi Andrey,
>>
>>
>>
>> FWIW, mono-traversable (http://hackage.haskell.org/package/mono-traversable) 
>> suggests decoupling IsSet and Funtor-like.
>>
>>
>>
>> In a nutshell, they define the IsSet class (in Data.Containers) with typical 
>> set operations like member and singleton, union and intersection. And then 
>> they tackle a (seemingly) independent problem of mapping monomorphic 
>> containers (like IntSet, ByteString, etc.) with a separate class MonoFunctor 
>> (in Data.MonoTraversable):
>>
>>
>>
>> class MonoFunctor mono where
>> omap :: (Element mono -> Element mono) -> mono -> mono
>>
>>
>>
>> And gazillion of instances for both polymorphic containers with a fixed type 
>> parameter and monomorphic ones.
>>
>>
>>
>> --
>>
>> Best wishes,
>>
>> Artem
>>
>>
>>
>> On Thu, 30 May 2019 at 20:11, Andrey Mokhov  
>> wrote:
>>
>> Hi all,
>>
>> I tried to use type classes for unifying APIs of several similar data 
>> structures and it didn't work well. (In my case I was working with graphs, 
>> instead of sets or maps.)
>>
>> First, you rarely want to be polymorphic over the set representation, 
>> because you care about performance. You really want to use that 
>> Very.Special.Set.insert because it has the right performance characteristics 
>> for your task at hand. I found only *one* use-case for writing polymorphic 
>> functions operating on something like IsSet: the testsuite. Of course, it is 
>> very nice to write a single property test like
>>
>> memberInsertProperty x set = (member x (insert x set) == True)
>>
>> and then use it for testing all set data structures that implement `member` 
>> and `insert`. Here you don't care about performance, only about correctness!
>>
>> However, this approach leads to problems with type inference, confusing 
>> error messages, and complexity. I found that it is much nicer to use 
>> explicit dictionary passing and write something like this instead:
>>
>> memberInsertProperty SetAPI{..} x set = (member x (insert x set) == True)
>>
>> where `member` and `insert` come from the SetAPI record via RecordWildCards.
>>
>> Finally, I'm not even sure how to create a type class covering Set and 
>> IntSet with the following two methods:
>>
>> singleton :: a -> Set a
>> map :: Ord b => (a -> b) -> Set a -> Set b
>>
>> singleton :: Int -> IntSet
>> map :: (Int -> Int) -> IntSet -> IntSet
>>
>> Could anyone please enlighten me about the right way to abstract over this 
>> using type classes?
>>
>> I tried a few approaches, for example:
>>
>> class IsSet s where
>> type Elem s
>> singleton :: Elem s -> s
>> map :: Ord (Elem t) => (Elem s -> Elem t) -> s -> t
>>
>> Looks nice, but I can't define the IntSet instance:
>>
>> instance IsSet IntSet where
>> type Elem IntSet = Int
>> singleton = IntSet.singleton
>> map = IntSet.map
>>
>> This fails with: Couldn't match type `t' with `IntSet' -- and indeed, how do 
>> I tell the compiler that in the IntSet case s ~ t in the map signature? 
>> Shall I add more associated types, or "associated constraints" using 
>> ConstraintKinds? I tried and failed, at various stage

Re: Container type classes

2019-05-29 Thread Iavor Diatchki
Hi,

having a common pattern for naming the operations certainly seems
nice.   I am ambivalent if we do this with a class, or just name the
operations the same way, and use the module system.  The type hackery
I was referring to was the type family for the set elements and map
keys you were referring to.It looks like the maps we have are
uniform enough that one type family per class does the job, so I think
the class you came with looks nice.

-Iavor
PS: the type hacker I was referring to was  having to add more type
families, for example if we had a map that can only store one type of
elements, but it looks like this is not the case here.


On Wed, May 29, 2019 at 3:48 AM Andreas Klebinger
 wrote:
>
> ghc-devs-requ...@haskell.org schrieb:
> > Hello,
> >
> > I think refactoring to use consistent naming is a good idea, but I am
> > not sure about the class idea.
> >
> > To see if it is viable, we should list the types in question and the
> > operations we'd like to overload.
> >
> > I find that with containers there tend to be two cases: either the
> > operations are similar but not exactly the same and you have to do
> > type hackery to make things fit, or you realize that you can just use
> > the same type in multiple places.
> >
> > Iavor
> The function prototype are already part of the merge request. See here:
> https://gitlab.haskell.org/ghc/ghc/blob/a0781d746c223636a90a0837fe678aab5b70e4b6/compiler/structures/Collections.hs
>
> As for the data structures in question these are:
> * EnumSet
> * Data.IntSet
> * Data.Set
> * UniqSet
> * UniqDSet
>
> * Data.IntMap
> * Data.Map
> * LabelMap
> * UniqFM
> * UniqDFM
> * UniqMap
>
> * Maybe the TrieMap Variants
>
> Maybe I missed some but these are all I can think of currently. But they
> are already plenty.
>
> Imo using type classes IS a kind of type hackery required "to make
> things fit".
> ___
> 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: Overloaded names for Map/Set?

2019-05-24 Thread Iavor Diatchki
Hello,

I think refactoring to use consistent naming is a good idea, but I am not
sure about the class idea.

To see if it is viable, we should list the types in question and the
operations we'd like to overload.

I find that with containers there tend to be two cases: either the
operations are similar but not exactly the same and you have to do type
hackery to make things fit, or you realize that you can just use the same
type in multiple places.

Iavor


On Fri, May 24, 2019, 07:12 Andreas Klebinger 
wrote:

> Hello devs,
>
> I would appreciate feedback on the idea in
> https://gitlab.haskell.org/ghc/ghc/merge_requests/934
>
> Maps/Sets in GHC for the most part offer the same basic functionality
> but their interfaces differ.
> In order to make this easier to work with I propose using overloading
> via IsSet/IsMap classes.
>
> The goal is to make working with these data structures simpler by having
> a uniform interface
> when it comes to names and argument orders.
>
> There are downsides, but to me they seem minor. Error messages can be
> more confusing when one
> get's the types wrong. We have to import the class to use it and the like.
> However overall I think making code easier by not having to remember the
> naming scheme + argument order
> for the different possible instances would make this worthwhile.
>
> But GHC isn't my project but one of the community so please voice your
> opinion on the matter on the
> merge request!
>
> Cheers
> Andreas
> ___
> 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: Processing MRs very slow?

2019-05-22 Thread Iavor Diatchki
Great thanks!  How can I have a look at Marge-bot's queue?

Perhaps it is worth updating Step 7 or 8 of
https://gitlab.haskell.org/ghc/ghc/wikis/working-conventions/fixing-bugs
to indicate that the reviewers should assign the MR to Marge-bot when
it is approved, and how one can check if that has happened.


On Wed, May 22, 2019 at 9:53 AM David Eichmann  wrote:
>
> Recently there have been some issues with CI that has slowed down
> merging. In particular a performance test (T9630) was failing on CI.
> That is fixed now and as of today Marge-Bot seems to be merging MRs
> again. I'll continue to monitor this in the coming days.
>
> Iavor, your MR was approved but not assigned to Marge-bot, and so was
> not in the merge queue. I'm not sure who has permission to do this, but
> you can always ping the approvers. In this case I've assigned to
> Marge-bot for you, and it will hopefully be merge soon.
>
> David Eichmann
>
> On 5/22/19 5:09 PM, Iavor Diatchki wrote:
> > Hello,
> >
> > I made a gitlab MR that adds two NOINLINE pragmas and some comments.
> > It's been about a week since my last push to the MR, and nothing has
> > happened since.
> >
> > Is there a way to check on what is its status:
> >- Is it stuck because I need to do something?
> >- Is it stuck because someone else needs to do something?
> >- Or is it just in the queue to be merged, in which case it would be
> > nice to know where in line it is, so I can see that there is progress,
> > and it is not just stuck.
> >
> > Given that this is such a simple MR, I am not too worried about
> > conflicts but a week long lag seems less than ideal for anything even
> > mildly complex.
> >
> > -Iavor
> >
> > PS: I just clicked on all the little check boxes from the
> > template---perhaps that's why things weren't progressing?
> > ___
> > ghc-devs mailing list
> > ghc-devs@haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
> --
> David Eichmann, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com
>
> Registered in England & Wales, OC335890
> 118 Wymering Mansions, Wymering Road, London W9 2NF, England
>
> ___
> 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: Bug or feature?

2019-05-22 Thread Iavor Diatchki
OK, I made #16684 to track the issue:
https://gitlab.haskell.org/ghc/ghc/issues/16684

Perhaps we should continue the discussion over there.

-Iavor

On Tue, May 21, 2019 at 10:18 PM Nicolas Frisby
 wrote:
>
> I'd be happy to raise a ticket, but it might take a few days -- work trip.
>
> On Tue, May 21, 2019, 01:55 Simon Peyton Jones  wrote:
>>
>> We have to be careful in how we define "equality" in the above sentence, 
>> including class constraints that (may) have superclass equality constraints.
>>
>>
>>
>> Indeed. That’s what happens now.
>>
>>
>>
>> I do think this would work.
>>
>>
>>
>> Cool.  Nick or Iavor: would you like to turn this conversation into a ticket?
>>
>>
>>
>> (Although it is technically user-facing, it is a very small corner and I’m 
>> not sure it would need a GHC proposal – others may want to comment.)
>>
>>
>>
>> Simon
>>
>>
>>
>> From: Richard Eisenberg 
>> Sent: 21 May 2019 09:43
>> To: Simon Peyton Jones 
>> Cc: Nicolas Frisby ; Iavor Diatchki 
>> ; ghc-devs@haskell.org; Ryan Scott 
>> 
>> Subject: Re: Bug or feature?
>>
>>
>>
>>
>>
>>
>>
>> On May 21, 2019, at 10:23 AM, Simon Peyton Jones via ghc-devs 
>>  wrote:
>>
>>
>>
>> But (A) looks sound to me.
>>
>>
>>
>> I like (A). (B) makes me nervous, too.
>>
>>
>>
>> > A. An implication is considered to “bind local equalities” iff it has at 
>> > least one given equality whose free variables are not all bound by the 
>> > same implication.
>>
>>
>>
>> We have to be careful in how we define "equality" in the above sentence, 
>> including class constraints that (may) have superclass equality constraints. 
>> I do think this would work.
>>
>>
>>
>> Richard
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Processing MRs very slow?

2019-05-22 Thread Iavor Diatchki
Hello,

I made a gitlab MR that adds two NOINLINE pragmas and some comments.
It's been about a week since my last push to the MR, and nothing has
happened since.

Is there a way to check on what is its status:
  - Is it stuck because I need to do something?
  - Is it stuck because someone else needs to do something?
  - Or is it just in the queue to be merged, in which case it would be
nice to know where in line it is, so I can see that there is progress,
and it is not just stuck.

Given that this is such a simple MR, I am not too worried about
conflicts but a week long lag seems less than ideal for anything even
mildly complex.

-Iavor

PS: I just clicked on all the little check boxes from the
template---perhaps that's why things weren't progressing?
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Bug or feature?

2019-05-20 Thread Iavor Diatchki
Hi,

thanks for the detailed response---I thought something like that might
be happening, which is why I thought I'd better ask before reporting a
bug.

I wonder how we might make the error message a little more user
friendly.   One idea would be to compute a couple of examples to show,
after an ambiguity check fails.

-Iavor

On Sat, May 18, 2019 at 7:03 AM Ryan Scott  wrote:
>
> Hi Iavor,
>
> This is a feature in the sense that it is an expected outcome of the
> OutsideIn(X) type inference algorithm (in particular, Section 5 of the
> corresponding paper [1]). I'll try to explain the issue to the best of
> my understanding.
>
> The tricky thing about the Q3 data type:
>
> data Q3 = forall a. Q3 (forall b. (F b ~ Int) => T a b)
>
> Is that there is a rank-n type with a /local/ equality constraint. In
> order to ensure that the type of the Q3 data constructor is never
> ambiguous, GHC tries to infer that Q3's type is always a subtype of
> itself. As a part of this, GHC attempts to solve the following
> implication constraint:
>
> forall a. forall b. (F b ~ Int) => (a ~ alpha)
>
> Where `alpha` is a unification variable. GHC tries to find a unique,
> most-general substitution that solves this constraint but ultimately
> gives up and reports the "untouchable" error message you observed.
>
> This is a bit strange, however. Upon first glance, this constraint
> would appear to have a unique solution: namely, [alpha |-> a]. Why
> doesn't GHC just use this? Ultimately, it's because OutsideIn(X) is
> conservative: there may exist constraints that admit a unique solution
> which it may fail to solve. This is explained in greater depth in
> Section 5.2 of the paper, but the essence of this restriction is
> because of the open-world assumption for type families. Namely, it's
> possible that your Q3 data type might later be linked against code
> which defines the following type family:
>
> type family G i a
> type instance G Int a = a
>
> If that were the case, then the implication constraint above would no
> longer have a unique solution, since there would exist another
> substitution [alpha |-> G (F b) a] that is incomparable with [alpha
> |-> a]. OutsideIn(X) was designed to only pick unique solutions that
> remain unique solutions even if more axioms (i.e., type family
> equations) are added, so for these reasons it fails to solve the
> implication constraint above.
>
> See also GHC issues #10651 [2], #14921 [3], and #15649 [4], which all
> involve similar issues.
>
> -
>
> I'm far from an expert on type inference, so I can't really offer a
> better inference algorithm that would avoid this problem. The best you
> can do, as far as I can tell, is to enable AllowAmbiguousTypes and
> hope for the best. Even then, you'll still run into situations where
> untouchability rears its ugly head, as in your `q3` definition. When
> that happens, your only available option (again, as far as I can tell)
> is to make use of TypeApplications. For example, the following /does/
> typecheck:
>
> q3 :: Q3
> q3 = Q3 @Bool t
>
> Hope that helps,
>
> Ryan S.
> -
> [1] 
> https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf
> [2] https://gitlab.haskell.org/ghc/ghc/issues/10651
> [3] https://gitlab.haskell.org/ghc/ghc/issues/14921
> [4] https://gitlab.haskell.org/ghc/ghc/issues/15649
> ___
> 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


Bug or feature?

2019-05-17 Thread Iavor Diatchki
Hello,

I've encountered some odd behavior related to quantification and type families,
but I am not sure if it is a bug or by design.

Here is an example which works fine:

> {-# Language ExistentialQuantification, RankNTypes, TypeFamilies #-}
>
> data T a b = T a
>
> t :: T Bool a
> t = T True
>
> data Q1 = forall a. Q1 (forall b. T a b)
>
> q1 :: Q1
> q1 = Q1 t

Now, suppose we wanted to constraint the universally quantified type of
the field.  This also works fine:

> data Q2 = forall a. Q2 (forall b. (b ~ Int) => T a b)
>
> q2 :: Q2
> q2 = Q2 t

However, things break down if the restriction involves a type family:

> type family F a
>
> data Q3 = forall a. Q3 (forall b. (F b ~ Int) => T a b)
>
> q3 :: Q3
> q3 = Q3 t

This causes some complaints about *a*, resulting from checking ambiguity.
If we `AllowAmbiguousTypes`, then the definition of `Q3` is accepted, but
`q3` fails with a similar error, complaining that GHC cannot match `a`
with `Bool` because it is "untouchable".

This seems confusing---I would have thought that when we use the `Q3`
constructor we are providing the value for `a` (e.g., it is `Bool`),
so I am not sure why GHC is trying
to match anything.

Any ideas?

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


Re: Website for viewing proposals

2019-05-10 Thread Iavor Diatchki
Having a read-only rendered version of all accepted proposals should
probably be pretty simple---we can even host it in the same repo using
"Github Pages".I don't know that we need anything more complex
than that.

On Thu, May 9, 2019 at 5:41 AM Joachim Breitner
 wrote:
>
> Hi,
>
> I looked into getting doi’s for our accepted proposals, but it looked
> harder than it should be.
>
> Building a nice web page from our repository and publishing it on
> GitHub pages, which can serve a custom domain like
> ghc-proposals.haskell.org would not be hard. Matthew even started a
> Makefile at some point that produces a reasonably nice output using
> sphinx.
>
> Maybe only reason why I am hesitant to do so is that there is a feature
> creep risk:
> We start with a webpage that shows accepted proposals,
> soon we’ll add functionality to list pending proposals and their status
> (why not? They are just a GitHub API call away),
> then we start using this page to actually drive the proposals (surely
> we can use this to tally the votes),
> and then we end up with a system that no longer has the “you just need
> to know GitHub to use it” property that made us build a Github-centric
> process in the first place.
>
> But maybe I am paranoid, and I should just set up the CI infrastructure
> for Matthew’s sphinx build.
>
> BTW, in hindsight, I regret that we renumber proposals after
> acceptance. It would be easier if they just retained the number of the
> PR (other proposal processes out there do that). But that ship has
> sailed.
>
> Cheers,
> Joachim
>
> Am Donnerstag, den 09.05.2019, 10:45 +0100 schrieb Matthew Pickering:
> > I want to cite a GHC proposal but linking to github for it doesn't
> > seem very official or permanent.
> >
> > Last year you also cited a proposal for your Haskell symposium paper
> > (https://arxiv.org/abs/1806.03476) but instead linked to the pull
> > request which also doesn't seem ideal to me.
> >
> > Matt
> >
> > On Thu, May 9, 2019 at 10:11 AM Simon Peyton Jones
> >  wrote:
> > > Interesting.  How would it differ from what we have (i.e. github's RST 
> > > viewer)?
> > >
> > > >  -Original Message-
> > > >  From: ghc-devs  On Behalf Of Matthew
> > > >  Pickering
> > > >  Sent: 09 May 2019 09:40
> > > >  To: GHC developers 
> > > >  Subject: Website for viewing proposals
> > > >
> > > >  Hi,
> > > >
> > > >  It would be useful if there was a canonical way to link and view GHC
> > > >  proposals rather than relying on github's RST viewer.
> > > >
> > > >  Can we set up a website, `ghc.haskell.org/proposals`, which is 
> > > > deployed to
> > > >  automatically when a new accepted proposal is merged?
> > > >
> > > >  FWIW, if the proposals process was also on gitlab then doing this
> > > >  deployment would be easy using our CI infrastructure but I don't know 
> > > > how
> > > >  to set up something similar on github.
> > > >
> > > >  Cheers,
> > > >
> > > >  Matt
> > > >  ___
> > > >  ghc-devs mailing list
> > > >  ghc-devs@haskell.org
> > > >  
> > > > https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.hask
> > > >  ell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-
> > > >  
> > > > devs&data=01%7C01%7Csimonpj%40microsoft.com%7C33b5834164a1436bd09308d6
> > > >  
> > > > d459edc0%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=vWx4R2xtV2%2BX7l
> > > >  RpM0weHo87NIc7pl0MoIiW76R%2BDdM%3D&reserved=0
> > ___
> > ghc-devs mailing list
> > ghc-devs@haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> --
> Joachim Breitner
>   m...@joachim-breitner.de
>   http://www.joachim-breitner.de/
>
> ___
> 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


Question about Gitlab MR workflow.

2019-05-08 Thread Iavor Diatchki
Hello,

I've just had a go at making a small MR on our new Gitlab system, and
I am a bit confused about the intended workflow.  I was following
these instructions :

https://gitlab.haskell.org/ghc/ghc/wikis/working-conventions/fixing-bugs

My question is about the steps after 2 (i.e., 3 and 4).  Step 5 about
the beer I already did :-)  Here was my experience so far:

1.  I made the changes I wanted yesterday over lunch: the change was
quite trivial, I added a NOINLINE pragma and some comments and I mage
the MR.

2. Sometime in the evening (half a day later!)  I got an e-mail from
the CI system that something had failed.  It was quite hard to tell
what had failed, and after poking around at the logs, it seemed like
it was some sort of spurious failures because things had timed out, I
think?

3. Today I got some feedback from a reviewer about some changes I
should make to the MR.  As I was working on those, I noticed that
every time I push to the MR, the CI is forking a new job.  I cancelled
some of those manually, to save on resources, as they already seem to
be taking half a day.

4. After making the changes, I noticed that Gitlab is asking me to
rebase my changes because, presumably, some other things have already
been merged.   It is easy enough to rebase my MR, but every time I do
so, this fires up a new CI job.   And, of course, this is going to
keep happening, until I am lucky enough to rebase just at the right
time?  This doesn't seem right.

So my questions are specifically about step 3 and 4:

   About 3:  wouldn't it make more sense to start firing up CI jobs
only after an MR has been approved for merging?

   About 4:  I really don't understand how this rebasing business is
intended to work: every time I rebase, I new CI job is fired up.  But,
presumably, while this is going, other things are going to be merged
with `master`, so I'd need to rebase again.   So, when would I ever
stop rebasing?
Furthermore, in my case the rebase is trivial, but with a larger
patch, doing multiple rebases seems like a lot of wasted work.

Any help would be appreciated!

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


Re: CI on forked projects: Darwin woes

2019-05-08 Thread Iavor Diatchki
I think there was the ghc-devops-group list, but I don't know if it is
still active, and I kind of like to not have to follow too many lists.

For example, I had also not realized that it is an option to push to
branches on the main project, and have been using my own fork,
so thanks for posting this here!

-Iavor


On Wed, May 8, 2019 at 11:40 AM Kevin Buhr  wrote:
>
> Over the past few days, I've submitted several merge requests from
> branches on my forked project (mostly because I didn't even realize
> pushing to a branch on the main project was an alternative).
>
> When those MRs run under CI, I've had a bunch of failures due to
> timeouts waiting on a darwin-x86_64 runner.  I was a little mystified
> that no other pipelines besides mine seemed to be having this problem,
> but I've come to understand that MRs submitted from branches on the main
> project use a different, larger set of runners than the shared runners
> used by MRs from branches on forked projects.
>
> Under my project, I can view the available shared runners under the
> "Settings" -> "CI/CD" -> "Runners" tab, and the problem seems to be that
> there's only one darwin runner ("b4bc6410" /
> mac-mini-x86_64-darwin-davxkc).  This machine is a trooper, but it
> unfortunately shares a circuit breaker with a toaster oven, so it goes
> offline every time someone wants a bagel, and the rest of the time it
> must be running CI for a few hundred GHC forks.
>
> I ended up deleting an (unreviewed) MR sourced from my branch, and
> pushing it to the main project and resubmitting just to get the CI to
> run.  (Admittedly, it failed, but at least not on darwin!)  I obviously
> don't want to do this with the merge requests that have already been
> reviewed.
>
> Is this a temporary problem?  Is there anything I can do other than keep
> retrying the darwin jobs every couple days?
>
> Also, is there a better place than "ghc-dev" to send these sorts of
> GitLab/CI issues?  I thought there might be a project dedicated to it,
> but if so I couldn't find it.
>
>
> --
> Kevin Buhr 
>
> ___
> 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: Cabal woes

2019-04-15 Thread Iavor Diatchki
Hello,

in case it is useful, here is how I think about what's happening with
cabal.   At present, `cabal-install` supports two different modes of
operation: the old style (aka `v1`) and the new style (aka `v2`) and---at
least for me---the two require a slightly different mental model of what is
going on.

In the old model, there is a user package database, and users would use
"cabal install" to install libraries their manually (e.g., using
`cabal-install`).   Later, when building various artifacts cabal would
prefer using the packages installed in the user's database.  This database
supported having multiple versions of a package, but NOT multiple builds of
the same version of a package (e.g., against different dependencies).  As a
result, builds would sometimes fail, because the dependencies of packages
would clash with each other (the unfortunate "cabal hell").

With the new model, there is still a "user" level location where libraries
are installed, but it is not really directly manipulated by the
user---rather it acts as more of a "cache" containing all versions of all
libraries every built and---crucially---it supports having multiple builds
of the same version of a package against different dependencies.   When
users build an artifact using the new style (aka "v2"), cabal automatically
checks if a suitable version of the library is already built in its cache,
and if not it adds it there.

The important difference between the two (at least in my mind) is that with
the new style, you never just install a library on its own.  Rather, you
install it as a part of a project, so Cabal can compute which version it
should install so that you get a version compatible with the rest of the
project.   Since in this model you never really install libraries directly,
the `install` command defaults to installing executables, which is what the
first error is trying to say.

So, if you want to try out `hspec` with the `v2` style of Cabal, you'd just
add it as a dependencies in the `cabal` file of your project, and then use
`cabal v2-build` to build the project, without having to install it
manually first.

I hope this helps,
-Iavor



On Mon, Apr 15, 2019 at 3:01 PM Simon Peyton Jones via ghc-devs <
ghc-devs@haskell.org> wrote:

> Thanks.  But alas I have no clue about whether I want a v1-install or a
> v2-install, nor how to achieve them if I knew what they were.  I just want
> to install ‘hspec’ so that I can use it when compiling a program.  How
> would I do that?
>
>
>
> The instructions here https://wiki.haskell.org/Cabal-Install just say
> “cabal install hspec” which is what I tried.  Those instructions are
> pointed to from here
> https://wiki.haskell.org/Cabal/How_to_install_a_Cabal_package, which in
> turn are pointed to from the main Cabal home page
> https://www.haskell.org/cabal/.
>
>
>
> I must be missing something.
>
>
>
> Simon
>
>
>
> *From:* Brandon Allbery 
> *Sent:* 15 April 2019 22:54
> *To:* Simon Peyton Jones 
> *Cc:* ghc-devs@haskell.org
> *Subject:* Re: Cabal woes
>
>
>
> I think you wanted v1-install to install a library into the user package
> database, since your cabal is 3.x and the v2-* commands are now the default
> (that is, you did what used to be cabal new-install or cabal v2-install).
>
>
>
> On Mon, Apr 15, 2019 at 5:47 PM Simon Peyton Jones via ghc-devs <
> ghc-devs@haskell.org> wrote:
>
> I’m trying to install ‘hspec’ on my WSL (Windows subsystem for Linux)
> system.
>
> But I fail; see below.
>
> For some reason cabal complains about installing a library.  (That seems
> peculiar – isn’t that what cabal is for?)  But it helpfully suggests adding
> –lib.
>
> Alas, cabal then crashes outright, which should never happen.
>
> So I’m stuck.  What should I do?
>
> Thanks
>
> Simon
>
>
>
> simonpj@MSRC-9870733:~$ cabal --version
>
> cabal-install version 3.0.0.0
>
> compiled using version 3.0.0.0 of the Cabal library
>
> simonpj@MSRC-9870733:~$ cabal install hspec
>
> Resolving dependencies...
>
> Up to date
>
> Warning: You asked to install executables, but there are no executables in
>
> target: hspec. Perhaps you want to use --lib to install libraries instead.
>
> simonpj@MSRC-9870733:~$ cabal install --lib hspec
>
> Resolving dependencies...
>
> Up to date
>
> Distribution/Simple/GHC.hs:1959:5-56: Irrefutable pattern failed for
> pattern Just ghcPkgProg
>
>
>
> simonpj@MSRC-9870733:~$ which ghc
>
> /opt/ghc/bin/ghc
>
> simonpj@MSRC-9870733:~$ which ghc-pkg
>
> /opt/ghc/bin/ghc-pkg
>
> simonpj@MSRC-9870733:~$
>
>
>
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> 

Re: Proposal: Don't read environment files by default

2019-03-29 Thread Iavor Diatchki
Hi Richard,

For use case 1)  we should probably make GHCi be more robust, and make it
notice that an environment file has become unusable, say so, and ignore it,
rather than refusing to work.  It is a bit of an odd way to synchronize
build artifacts though.

For 2), I like global databases too, and I think that this system is very
compatible with it---you can think of the "global" environment as a default
project that GHCi uses when there is no other project around.  I believe
something like that is already being developed.  In the mean-time, however,
I've just been using one "sand-box" cabal project that has just a cabal
file, and no source files---when I want to try stuff out, I just go to that
project and fire up `ghci`.  It avoids cabal hell as you can easily control
the versions of the libraries you need, if you care.  It is also cool, in
that you can put it on github, and be able to easily recreate the same
environment on different machines.  And having used that for a while, I've
noticed that perhaps I don't really want a global project, as I've evolved
a couple of different "sand-boxes" for different topics that I commonly
play around with.

As for your relevant scenario:  couldn't you just add the packages you want
to use to your cabal file and ask it to build them for you?  Then you'd
know what version of the package you are actually experimenting with.  I
haven't actually run into this issue much, so I can't recall what GHCi says
if you try to use a module from a package that is not part of the current
context, but it sounds like we may want to improve its message, if the
current situation is confusing.




On Thu, Mar 28, 2019 at 12:26 PM Richard Eisenberg  wrote:

>
>
> On Mar 28, 2019, at 3:09 PM, Herbert Valerio Riedel 
> wrote:
>
> That being said, I'd be more interested to know the actual problems
> people are having
>
>
> I've run into two problems. I don't expect others to run into these
> particular problems, as my workflows are likely different than others', but
> both of these bit me independently.
>
> 1. I use two different machines regularly. I keep my files in sync between
> them using Dropbox. Yet, the Haskell installations between are not
> identical. Even if the GHC version is the same, it's quite likely that some
> library, etc., has been installed at a different version on the two
> machines. (Sometimes, even the GHC is different.) I did some work on a
> project on machine 1; this produced an environment file. Then, machine 2's
> window happened to be in the project directory. I wanted to spin up GHCi to
> check the type of, e.g., traverse. But GHCi wouldn't launch! This is
> because machine 1's work produced the environment file which invisibly got
> copied to machine 2 (via Dropbox) and then GHCi tried to respect the
> environment file, even though I had no interest in interacting with that
> particular project at the moment. Frustration and confusion ensued.
>
> 2. I get pilloried every time I say it, but I vastly prefer global package
> databases to local ones. This is because, usually, I'm compiling individual
> Haskell files and not projects. These Haskell files are snippets of code I
> look at in order to spot a GHC bug and files students email me seeking help
> on. I therefore like to build up a healthy set of libraries in my global
> package database so I can just test-drive these files, without worrying
> about managing dependencies. (It is true that I sometimes run into
> old-style "cabal hell", but I also accept that this is an unavoidable
> consequence of using the global package database. By the time this happens,
> a new GHC has been released anyway, and I use the outdated package database
> as an excuse to upgrade.)
>
>   The actual relevant scenario is this: I open GHCi to load some files
> from a project, and I want to experiment with them. But I realize that I
> want to import a few modules from packages not otherwise used in the
> project (e.g., the 'extra' package) in order to conduct my experiments. But
> I can't do this, because the env file tells me I can't. Frustration and
> confusion ensued.
>
> I have a better understanding of all this now -- and the knowledge to
> disable these features -- but this is how I came to dislike these env
> files. In both cases, it was because I wanted to interact with Haskell in a
> way that wasn't fully encapsulated within a project. Perhaps in a "real
> company", this wouldn't happen, but many Haskellers are not in real
> companies. :)
>
> Richard
> ___
> 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: Proposal: Don't read environment files by default

2019-03-28 Thread Iavor Diatchki
I am quite confused as to how people are using `ghci` without loading the
environment files, at least in the context of cabal v2 (aka "new cabal").
 When you run `ghci` on its own, unless you load an environment file, you
would only have access to globally installed packages, which is almost
never what you want.   What is the workflow that this proposal optimizes?

The default behavior should be what's commonly useful and, in my
experience, when I run GHCi in the context of a project, I pretty much
always want it to load the environment associated with the project.   It is
incredibly useful when you are working on a project where there are
multiple broken modules (e.g., during refactoring), and you want to fix
them one at a time, in the order that makes sense to you.

-Iavor


On Thu, Mar 28, 2019 at 10:02 AM Bardur Arantsson 
wrote:

> On 28/03/2019 14.58, Oleg Grenrus wrote:
> > There is. Add
> >
> > write-ghc-environment-files: never
> >
> > to your ~/.cabal/config assuming you have cabal-insall-2.4.1.0 or later.
> >
>
> That doesn't really work if you actually want to be able to use both
> ways of working, does it? That same thing applies to
>
>   export GHC_ENVIRONMENT=-
>
> which someone else posted, but at least that can be done by tooling
> before invoking ghc. It's odd to have to change a global setting to
> avoid this. (However, thanks for the hints -- I'll be setting that
> GHC_ENVIRONMENT from now on.)
>
> +1 for changing the default.
>
> It seems really weird to force other tooling to opt out when this could
> easily be solved by just having
>
>cabal ghci
>cabal ghc
>
> commands which set up the environment properly and tell users to use
> that if they want to use cabal's environment files. FWIW, I also see
> e.g. ghc as low-level tooling akin to the plain 'gcc' command whereas
> e.g. cabal or stack are more like cmake + make/ninja, i.e. it's not
> something users should really be running unless they know what they're
> doing *and* it should be as tooling-friendly as possible.
>
> Regards,
>
> ___
> 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: Proposal: Don't read environment files by default

2019-03-28 Thread Iavor Diatchki
I used to be confused by the environment files too until I figured out what
they are, and now I use them all the time.

It is really nice to be able to have the "old fashioned" way of just
running ghci and having it be aware of the current project your are in.

To me, it really makes sense to be aware of the context by default.  To
reduce confusion, we could make GHCi be more explicit about telling the
user that it loaded a context, but I think 99% of the time I want it to so.
So I'd prefer to have a flag to disable the behavior for the 1%, but the
default should load the context IMHO

Iavor




On Thu, Mar 28, 2019, 08:49 Richard Eisenberg  wrote:

>
>
> On Mar 28, 2019, at 10:31 AM, Herbert Valerio Riedel 
> wrote:
>
> I for one would hate to remove what I consider a useful feature
>
>
> I don't see anyone is asking for a feature removal here. This thread seems
> to be more about how to set a default.
>
> I personally find it surprising for a tool like a compiler to be
> directory-sensitive. But I've now learned that with `export
> GHC_ENVIRONMENT=-` in my profile, my compiler indeed isn't
> directory-sensitive. Furthermore, I've learned how to suppress the env
> files entirely with `write-ghc-environment-files: never` in my
> ~/.cabal/config. So I'm not actually all too bothered by this anymore. I
> retain my opinion that directory-sensitivity is a poor design (it's
> precisely what threw me off Stack the first time I tried it) for
> compiler-like tools, but perhaps that ship has sailed, as I agree that
> changing this now may lead to a poor user experience.
>
> Richard
> ___
> 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: Gitlab notes

2019-01-08 Thread Iavor Diatchki
One other thing:

At least on Github, using the button on the site to merge a request
always creates a proper merge (not a rebase), so the history won't be
straight if we do things that way.  I believe the reasoning is that in this
way, you have record of who did the merging.
I am not sure if this holds for Gitlab, but we should look into it, if
we want to keep the straight history.




On Tue, Jan 8, 2019 at 10:44 AM Simon Peyton Jones 
wrote:

> I like your notes.  I’ll add them.
>
>
>
> I think that ideally
>
>- We’d keep a straight-line history for master
>- And hence we have to accept force-push to user branches.
>- Surely we can treat the user branches much as we do HEAD today?
>That is, always  pull before pushing; and only force push if you know that
>you have just pulled; and then rebased, squashed or whatever.
>- In any case the common case is that only one person is pushing to a
>user branch
>
>
>
> It would be good to agree our normal protocol here.
>
>
> Simon
>
>
>
> *From:* Iavor Diatchki 
> *Sent:* 08 January 2019 18:10
> *To:* Simon Peyton Jones 
> *Cc:* ghc-devs 
> *Subject:* Re: Gitlab notes
>
>
>
> Hello,
>
>
>
> a couple of notes about the use of `git` here, which are probably more
> relevant if you collaborate with other people on a branch:
>
>
>
>1. In general, I think that the model is that you create the branch
> when you start working on something, and you don't really need
>
>   to do a merge request until later, when you are ready for review.
>
>
>
>2. when you are pushing your branch to the remote (i.e., git-lab), you
> probably want to say that you branch should "track" the remote by providing
> the `-u` flag:
>
>
>
>git push -u origin wip/spj-wibbles
>
>
>
>  This makes `git` remember the association between your local branch,
> and the one that lives on git-lab, so later if you can just say `git pull`
> and `git push` and
>
>  `git` will know what remote you are talking about.
>
>
>
> 3. You shouldn't really force push to a remote, especially if you are
> collaborating with other people.
>
>If you want to integrate your changes with the current HEAD (aka
> `master`), you may want to merge it into your working branch.
>
>
>
> 4. Once you are finished with the changes and they are ready for
> review, you can prepare them by doing any of these as needed:
>
> a)  rebasing to a more relevant starting point (perhaps even the
> current `master`),
>
> b) squashing commits as necessary---for simple changes, one should
> probably end up with a single commit.
>
>   Since those "rewrite history", you are essentially making a new
> branch, and you could submit *that* for review.  Alternatively,
>
>   you could reuse your working branch (a bit of a hack), and then
> you'd have to "force" push.
>
>
>
> 5. When everything is ready for review, then you create the MR for the
> appropriate branch (either the new review one, or
>
> your working one, if you chose to reuse it)
>
>
>
>  6. You can continue evolving the branch as usual based on feedback
> from the reviews.
>
>
>
>  7. Once all the reviewers are happy, you can prepare the branch for
> merging with `master` as in 4.
>
>
>
>  I believe in the past GHC has tried to maintain a "straight line"
> history model, where changes are always made
>
>  on top of the current `master` branch (i.e., there are no visible
> merges).  If we are still doing that, then you'd
>
>  have to rebase your reviewed changes on top of `master` in
> preparation for merging.
>
>
>
> I didn't add this to the wiki, as they are subjective, but they reflect my
> understanding of how systems like `git-lab`
>
> are intended to be used.
>
>
>
> -Iavor
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
> On Tue, Jan 8, 2019 at 8:30 AM Simon Peyton Jones via ghc-devs <
> ghc-devs@haskell.org> wrote:
>
> Friends
>
> I’ve added a Wiki page to summarise things I’ve learned about Gitlab.
> Please do correct any errors I’ve made!
>
> https://ghc.haskell.org/trac/ghc/wiki/WorkingConventions/GitLabSPJ
> <https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fghc.haskell.org%2Ftrac%2Fghc%2Fwiki%2FWorkingConventions%2FGitLabSPJ&data=02%7C01%7Csimonpj%40microsoft.com%7C0f8493cdde724d53f26b08d675948b0f%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63682567818

Re: Gitlab notes

2019-01-08 Thread Iavor Diatchki
Hello,

a couple of notes about the use of `git` here, which are probably more
relevant if you collaborate with other people on a branch:

   1. In general, I think that the model is that you create the branch when
you start working on something, and you don't really need
  to do a merge request until later, when you are ready for review.

   2. when you are pushing your branch to the remote (i.e., git-lab), you
probably want to say that you branch should "track" the remote by providing
the `-u` flag:

   git push -u origin wip/spj-wibbles

 This makes `git` remember the association between your local branch,
and the one that lives on git-lab, so later if you can just say `git pull`
and `git push` and
 `git` will know what remote you are talking about.

3. You shouldn't really force push to a remote, especially if you are
collaborating with other people.
   If you want to integrate your changes with the current HEAD (aka
`master`), you may want to merge it into your working branch.

4. Once you are finished with the changes and they are ready for
review, you can prepare them by doing any of these as needed:
a)  rebasing to a more relevant starting point (perhaps even the
current `master`),
b) squashing commits as necessary---for simple changes, one should
probably end up with a single commit.
  Since those "rewrite history", you are essentially making a new
branch, and you could submit *that* for review.  Alternatively,
  you could reuse your working branch (a bit of a hack), and then you'd
have to "force" push.

5. When everything is ready for review, then you create the MR for the
appropriate branch (either the new review one, or
your working one, if you chose to reuse it)

 6. You can continue evolving the branch as usual based on feedback
from the reviews.

 7. Once all the reviewers are happy, you can prepare the branch for
merging with `master` as in 4.

 I believe in the past GHC has tried to maintain a "straight line"
history model, where changes are always made
 on top of the current `master` branch (i.e., there are no visible
merges).  If we are still doing that, then you'd
 have to rebase your reviewed changes on top of `master` in
preparation for merging.

I didn't add this to the wiki, as they are subjective, but they reflect my
understanding of how systems like `git-lab`
are intended to be used.

-Iavor













On Tue, Jan 8, 2019 at 8:30 AM Simon Peyton Jones via ghc-devs <
ghc-devs@haskell.org> wrote:

> Friends
>
> I’ve added a Wiki page to summarise things I’ve learned about Gitlab.
> Please do correct any errors I’ve made!
>
> https://ghc.haskell.org/trac/ghc/wiki/WorkingConventions/GitLabSPJ
>
> Thanks
>
> Simon
> ___
> 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: Current Stable Release = 8.6.2 on haskell.org

2018-12-23 Thread Iavor Diatchki
Given that 8.6.3 does not work at all on Windows (seems to hang when TH is
involved), we should probably not make it the current stable release. See
16071, I also just run into that and had to revert to 8.6.2.

Iavor

On Sun, Dec 23, 2018, 4:08 PM Ben Gamari  Artem Pelenitsyn  writes:
>
> > Hello devs,
> >
> > I assume, the version of the current release should be bumped up to 8.6.3
> > here [1]?
> >
> Yes, quite right.
>
> I'll handle this soon.
>
> 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


Re: Using GHC Core as a Language Target

2018-10-25 Thread Iavor Diatchki
Hello,

I have not done what you are asking, but here is how I'd approach the
problem.

1. Assuming you already have some Core, you'd have to figure out how to
include it with the rest of the GHC pipeline:
* A lot of the code that glues everything together is in
`compiler/main`. Modules of interest seem to be `DriverPipeline`,
`HscMain`, and `PipelineMoand`
* A quick looks suggests that maybe you want to call `hscGenHardCode`
in `HscMain`, with your core program inside the `CgGuts` argument.
* Exactly how you setup things probably depends on how much of the rest
of the Haskell ecosystem you are trying to integrate with (separate
compilation, avoiding recompilation, support for packages, etc.)

2. The syntax for Core is in `compiler/coreSyn`, with the basic AST being
in module `CoreSyn`.   Module `MkCore` has a lot of helpers for working
with core syntax.

3. The "desugarer" (in `compiler/deSugar`) is the GHC phase that translates
the front end syntax (hsSyn) into core, so that should have lots of
examples of how to generate core.

Cheers,
-Iavor







On Mon, Oct 22, 2018 at 1:46 AM Ara Adkins  wrote:

> Hey All,
>
> I was chatting to SPJ about the possibility of using GHC Core + the rest
> of the GHC compilation pipeline as a target for a functional language, and
> he mentioned that asking here would likely be more productive when it comes
> to the GHC API.
>
> I'm wondering where the best place would be for me to look in the API for
> building core expressions, and also whether it is possible to trigger the
> GHC code-generation pipeline from the core stage onwards.
>
> Best,
> Ara
> ___
> 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: Parser.y rewrite with parser combinators

2018-10-08 Thread Iavor Diatchki
Hello,

my experience with complex parsers written using parsing combinators is
that they tend to be quite difficult to modify and have any kind of
assurance that now you haven't broken something else.   While reduce-reduce
errors are indeed annoying, you at least know that there is some sort of
issue you need to address.   With a combinator based parser, you basically
have to do program verification, or more pragmatically, have a large test
suite and hope that you tested everything.

I think the current approach is actually quite reasonable:  use the Happy
grammar to parse out the basic structure of the program, without trying to
be completely precise, and then have a separate pass that validates and
fixes up the results.   While this has the draw-back of some constructors
being in the "wrong place", there are also benefits---namely we can report
better parse errors.  Also, with the new rewrite of HsSyn, we should be
able to mark such constructors as only usable in the parsing pass, so later
passes wouldn't need to worry about them.

-Iavor











On Mon, Oct 8, 2018 at 2:26 PM Simon Peyton Jones via ghc-devs <
ghc-devs@haskell.org> wrote:

> I'm no parser expert, but a parser that was easier to understand and
> modify, and was as fast as the current one, sounds good to me.
>
> It's a tricky area though; e.g. the layout rule.
>
> Worth talking to Simon Marlow.
>
> Simon
>
>
>
> | -Original Message-
> | From: ghc-devs  On Behalf Of Vladislav
> | Zavialov
> | Sent: 08 October 2018 21:44
> | To: ghc-devs 
> | Subject: Parser.y rewrite with parser combinators
> |
> | Hello devs,
> |
> | Recently I've been working on a couple of parsing-related issues in
> | GHC. I implemented support for the -XStarIsType extension, fixed
> | parsing of the (!) type operator (Trac #15457), allowed using type
> | operators in existential contexts (Trac #15675).
> |
> | Doing these tasks required way more engineering effort than I expected
> | from my prior experience working with parsers due to complexities of
> | GHC's grammar.
> |
> | In the last couple of days, I've been working on Trac #1087 - a
> | 12-year old parsing bug. After trying out a couple of approaches, to
> | my dismay I realised that fixing it properly (including support for
> | bang patterns inside infix constructors, etc) would require a complete
> | rewrite of expression and pattern parsing logic.
> |
> | Worse yet, most of the work would be done outside Parser.y in Haskell
> | code instead, in RdrHsSyn helpers. When I try to keep the logic inside
> | Parser.y, in every design direction I face reduce/reduce conflicts.
> |
> | The reduce/reduce conflicts are the worst.
> |
> | Perhaps it is finally time to admit that Haskell syntax with all of
> | the GHC cannot fit into a LALR grammar?
> |
> | The extent of hacks that we have right now just to make parsing
> | possible is astonishing. For instance, we have dedicated constructors
> | in HsExpr to make parsing patterns possible (EWildPat, EAsPat,
> | EViewPat, ELazyPat). That is, one of the fundamental types (that the
> | type checker operates on) has four additional constructors that exist
> | due to a reduce/reduce conflict between patterns and expressions.
> |
> | I propose a complete rewrite of GHC's parser to use recursive descent
> | parsing with monadic parser combinators.
> |
> | 1. We could significantly simplify parsing logic by doing things in a
> | more direct manner. For instance, instead of parsing patterns as
> | expressions and then post-processing them, we could have separate
> | parsing logic for patterns and expressions.
> |
> | 2. We could fix long-standing parsing bugs like Trac #1087 because
> | recursive descent offers more expressive power than LALR (at the cost
> | of support for left recursion, which is not much of a loss in
> | practice).
> |
> | 3. New extensions to the grammar would require less engineering effort.
> |
> | Of course, this rewrite is a huge chunk of work, so before I start, I
> | would like to know that this work would be accepted if done well.
> | Here's what I want to achieve:
> |
> | * Comparable performance. The new parser could turn out to be faster
> | because it would do less post-processing, but it could be slower
> | because 'happy' does all the sorts of low-level optimisations. I will
> | consider this project a success only if comparable performance is
> | achieved.
> |
> | * Correctness. The new parser should handle 100% of the syntactic
> | constructs that the current parser can handle.
> |
> | * Error messages. The new error messages should be of equal or better
> | quality than existing ones.
> |
> | * Elegance. The new parser should bring simplification to other parts
> | of the compiler (e.g. removal of pattern constructors from HsExpr).
> | And one of the design principles is to represent things by dedicated
> | data structures, in contrast to the current state of affairs where we
> | represent patterns as expressions, data constructor 

Discussion on proposal #99: forall {k}

2018-04-30 Thread Iavor Diatchki
Hello,

As a shepherd for proposal #99, I'd like to kick off the discussion.  The
full proposal is available here:
https://github.com/goldfirere/ghc-proposals/blob/explicit-specificity/proposals/-explicit-specificity.rst

Summary: allows programmers to write `forall {x}` instead of `forall x` in
type signatures.  The meaning of the braces is that this parameter cannot
be instantiated with an explicit type application and will always be
inferred.  The motivation is to shorten explicit type applications by
skipping parameters that are known to be inferable, the common example
being omitting the kinds in signatures with poly kinds.

As I understand it, the main motivation for this proposals is to give
programmers more flexibility when instantiating type variables, with a less
noisy syntax.   While the proposed solution might work in some situations,
I am unconvinced that it is the best way to address the issue in general,
for the following reasons:

  1. It requires that programmers commit at declaration time about which
arguments will be inferred, and which may be inferred or specified.   While
in some cases this may be an easy decision to make, in many cases this
really is a decision which should be made at the use site of a function
(e.g., I'd like to provide argument X, but would like GHC to infer argument
Y).

  2. It still requires that programmers instantiate arguments in a fixed
order,  which is sometimes dictated by the structure of the type itslef.
Here is, for example, what the proposal suggests to do if you want to
provide type before a kind:

typeRep4 :: forall {k} (a :: k) k'. (k ~ k', Typeable a) => TypeRep a

While technically this is not wrong, it is not exactly elegant.

I think that we should reject this proposal, and try to come up with a more
comprehensive solution to the problem.

One alternative design is to allow programmers to instantiate type
variables by name.  This is much more flexible as it allows programmers to
instantiate whichever variables they want, and in whatever order.  We've
been doing this in Cryptol for a long time, and it seems to work really
well.

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


Question about TypeInType

2018-04-12 Thread Iavor Diatchki
Hello,

I was experimenting with TypeInType and run into a problem, that can be
reduced to the following example.  Does anyone have any insight on what
causes the error, in particular why is `IxKind` not being reduced?

-Iavor


{-# Language TypeInType, TypeFamilies #-}

module Help where

import Data.Kind

type family IxKind (m :: Type) :: Type
type family Value (m :: Type) :: IxKind m -> Type

data T (k :: Type) (f :: k -> Type)

type instance IxKind (T k f) = k
type instance Value (T k f) = f

{-
[1 of 1] Compiling Help ( Desktop/Help.hs, interpreted )
Desktop/Help.hs:13:31: error:
• Expected kind ‘IxKind (T k f) -> *’, but ‘f’ has kind ‘k -> *’
• In the type ‘f’
  In the type instance declaration for ‘Value’
   |
13 | type instance Value (T k f) = f
   |   ^
Failed, no modules loaded.
-}
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: pattern signatures

2018-01-05 Thread Iavor Diatchki
Well, as you say, "pattern signature" makes sense for both, so I would
expect to use context to disambiguate.  If I wanted to be explicit about
which one I meant, I'd use:

a) "Pattern synonym signature"
b) "Signature on a pattern"

-Iavor




On Fri, Jan 5, 2018 at 1:12 PM Joachim Breitner 
wrote:

> Hi,
>
> Am Freitag, den 05.01.2018, 13:42 -0500 schrieb Brandon Allbery:
> > Further complicated by the fact that that form used to be called a
> > "pattern signature" with accompanying extension, until that was
> > folded into ScopedTypeVariables extension.
>
> which I find super confusing, because sometimes I want a signature on a
> pattern and it is counter-intuitive to me why I should not longer use
> the obviously named PatternSignatures extension but rather the at first
> glance unrelated ScopedTypeVariable extension.
>
> But I am derailing the discussion a bit.
>
> Cheers,
> Joachim
>
> --
> Joachim Breitner
>   m...@joachim-breitner.de
>   http://www.joachim-breitner.de/
> ___
> 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: True multi stage Haskell

2017-11-17 Thread Iavor Diatchki
Hello Tim,

I don't know the answers to your questions exactly, but I've played around
with something that I think might be related, so I thought I'd share.   The
example code is here:

https://github.com/GaloisInc/galua/blob/master/galua-jit/src/Galua/Micro/Compile.hs

This module contains a function that compiles (at runtime) a Haskell module
represented as a String to the value of whatever `main` happened to be
defined in this module.
Actually, in this case the expression is taken as a `Doc` , which is the
result of pretty printing something, but this doc is simply "show"-ed to
make a string (see `modText`).

The function works in roughly two steps:
1. Compile the module:
1.1. Setup some compiler flags, this has to do with the
dependencies of the module (i.e., what packages it depends on, etc)
1.2. Define a "target":  this is what GHC will be compiling.  There
is a bit of weirdness here:  GHC can take the input to compile either from
a text file, or from an in-memory buffer.  The second is what we want
here.  Unfortunately, for some reason GHC still insists on there being a
file around (its contents is completely irrelevant) I think it just want to
check when it was last modified :-)This is why we create an empty
file. This is something that should probably be fixed in GHC.
1.3 Load all the targets:  this is what will actually compile the
module
2. Get the value of `main` in this module:  this is done in the
`Succeed` branch of the case, where we create an expression `M.main` and
tell GHC to evaluate it.

Depending on how you need things to be setup, just the second step might be
enough (i.e., call `compileExpr`).   You'd still need to do enough to tell
GHC in what context it will be compiling the expression though.

I am not an expert on this topic, but I'd be happy to try to answer more
questions if I can.

-Iavor



On Fri, Nov 17, 2017 at 10:42 AM Matthew Pickering <
matthewtpicker...@gmail.com> wrote:

> Hi Tim,
>
> When you say "multi-stage programming language" do you have a specific
> calculus in mind? I think this can mean lots of different things to
> different people.
>
> This is a topic I have been interested in recently.
>
> Cheers,
>
> Matt
>
> On Fri, Nov 17, 2017 at 6:05 PM, Tim Sheard  wrote:
> > After many years of hoping someone else would do this, I would like to
> > make GHC into a true multi-stage programming language. Here is how I
> > thought I might approach this.
> >
> > 1) Use the GHC as a library module.
> > 2) Use the LLVM backend.
> >
> > I have no experience with either of these tools.
> > Lets start simple, How would I write functions like
> >
> > compile :: String -> IO PtrToLLVMCode  -- where the string is a small
> > Haskell program.
> > llvmCompile :: PtrToLLVMCode -> IO PtrToMachineCode
> > jumpTo:: PtrToMachineCode -> IO ans   -- where ans is the "type" of the
> > string.
> >
> >
> > Any thoughts on how to get started? What papers to read, examples to look
> > at?
> >
> > I'd love to move to some more disciplined input type, a sort of (mono)
> typed
> > program
> > representation (with similar complexity) to Template Haskell Exp type.
> >
> > where (Exp t) is a data structure representing a Haskell program of type
> t.
> >
> > All offers of advice accepted. I'm trying to get started soon, and good
> > advice
> > about what to avoid is especially welcome.  If any one wanted to help
> with
> > this,
> > that would be great.
> >
> > Tim Sheard
> >
> > ___
> > 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
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Building the docs, again

2017-11-01 Thread Iavor Diatchki
Hello,

I was talking about the user manual.   I imagine that the situation I was
in is quite common---you've just implemented some small feature, and you
want to write some documentation about it.  While working on the
documentation, I want to rebuild the manual quickly, so that I can see what
it looks like, and make sure that links etc.

So I think it would be very important for Hadrian to have some high-level
targets equivalent to the current `make html` etc. rather than having to
ask it to rebuild a specific file somewhere in the build tree.

The confusion with my previous e-mail was caused because I hadn't realized
what happens when building the documentation is disabled, namely:
1. There are multiple places to check if the documentation is actually
disabled
2. When the documentation is disabled, the build targets disappear,
rather than change their behavior to say "Docs are disabled, I am not going
to build them, do X if you want them build".

So the issue is more of a usability one.

After I sent the e-mail to the list I realized that this all is documented
online, so that's nice at least, but---in general---I think it would be
nice if we could avoid such surprised, rather than having to document them
in a separate place.

-Iavor






On Wed, Nov 1, 2017 at 11:07 AM Patrick Dougherty 
wrote:

> I spent some time with the docs this summer, and wrote a fair bit of the
> Hadrian documentation building code. So maybe I can shed some light.
>
> The question is which docs do you want to build? The library documentation
> relies on the haddock executable, which is one of the last targets in the
> entire build. Also, IIRC, creating the nice links and references is
> somewhat tangled up with actually building the libraries. So it's not
> possible to avoid building GHC if you want the haddocks.
>
> On the other hand, you can build just the user's guide using Hadrian. You
> can build any sphinx html target like this:
>
> ./build.sh _build/docs/html/users_guide/index.html
>
> Or pdf with:
>
> ./build.sh _build/docs/pdfs/users_guide.pdf
>
> While not the cleanest, it does work. So, I think the only way you can
> skip building GHC is using Hadrian for sphinx targets.
>
> Until recently, the users guide did depend on building all of GHC.. I
> believe the make-based build just doesn't know about this change? I think I
> looked into updating it, but determined that it would be easier just to
> update Hadrian instead. I'm a little foggy on the details at this point.
>
> Best,
> Patrick
>
> On Nov 1, 2017, at 7:13 AM, Andrey Mokhov  > wrote:
>
> > Maybe Hadrian will help here?
>
>
>
> Hadrian can build documentation in various formats but the current
> implementation is very coarse-grain: we either build all possible docs or
> no docs at all. It would be relatively easy to add more fine-grain
> documentation targets and modes. If someone could design/describe the
> requirements in a ticket that would be great.
>
>
>
> Cheers,
>
> Andrey
>
>
>
>
>
> *From:* Simon Peyton Jones [mailto:simo...@microsoft.com
> ]
> *Sent:* 01 November 2017 08:28
> *To:* Iavor Diatchki ; ghc-devs@haskell.org;
> Andrey Mokhov 
> *Subject:* RE: Building the docs, again
>
>
>
> It is quite confusing that we can be setting the same variable to
> different values in different places.   It would also be quite helpful if
> we modified the Makefile to say `documentation build target is disabled` or
> some such, rather then going ahead and building the whole of GHC, only at
> the end to inform me that it doesn't know what is `html`.
>
> Maybe Hadrian will help here?
>
>
>
> Simon
>
>
>
> *From:* ghc-devs [mailto:ghc-devs-boun...@haskell.org
> ] *On Behalf Of *Iavor Diatchki
> *Sent:* 31 October 2017 21:49
> *To:* ghc-devs@haskell.org
> *Subject:* Re: Building the docs, again
>
>
>
> Hello,
>
>
>
> never mind, I figured it out---apparently the build targets were disabled
> for the `quick` flavor, which I was using.
>
>
>
> It is quite confusing that we can be setting the same variable to
> different values in different places.   It would also be quite helpful if
> we modified the Makefile to say `documentation build target is disabled` or
> some such, rather then going ahead and building the whole of GHC, only at
> the end to inform me that it doesn't know what is `html`.
>
>
>
> -Iavor
>
>
>
>
>
>
>
> On Tue, Oct 31, 2017 at 2:26 PM Iavor Diatchki 
> wrote:
>
> Hello,
>
>
>
> sometime ago, I asked if it is possible to build just the GHC docs,
> without building the compiler.  I was told to just run `make html`.  This
> does not a

Re: Building the docs, again

2017-10-31 Thread Iavor Diatchki
Hello,

never mind, I figured it out---apparently the build targets were disabled
for the `quick` flavor, which I was using.

It is quite confusing that we can be setting the same variable to different
values in different places.   It would also be quite helpful if we modified
the Makefile to say `documentation build target is disabled` or some such,
rather then going ahead and building the whole of GHC, only at the end to
inform me that it doesn't know what is `html`.

-Iavor



On Tue, Oct 31, 2017 at 2:26 PM Iavor Diatchki 
wrote:

> Hello,
>
> sometime ago, I asked if it is possible to build just the GHC docs,
> without building the compiler.  I was told to just run `make html`.  This
> does not appear to work, the command seems to just start building GHC.
> What am I doing wrong?
>
> Here is the output I see, running the command from the root of the GHC
> tree.
>
> > make html V=0
> ===--- building phase 0
> make --no-print-directory -f ghc.mk phase=0 phase_0_builds
> make[1]: Nothing to be done for 'phase_0_builds'.
> ===--- building phase 1
> make --no-print-directory -f ghc.mk phase=1 phase_1_builds
>   HC [stage 0] compiler/stage1/build/BufWrite.o
>   HC [stage 0] compiler/stage1/build/Pretty.o
> compilation IS NOT required
>   HC [stage 0] compiler/stage1/build/PprColour.o
> compilation IS NOT required
>   HC [stage 0] compiler/stage1/build/Outputable.o
> compilation IS NOT required
>   HC [stage 0] compiler/stage1/build/Json.o
> compilation IS NOT required
>   HC [stage 0] compiler/stage1/build/SrcLoc.o
> compilation IS NOT required
>   HC [stage 0] compiler/stage1/build/BasicTypes.o
> compilation IS NOT required
>   HC [stage 0] compiler/stage1/build/Unique.o
>   HC [stage 0] compiler/stage1/build/Packages.o-boot
> compilation IS NOT required
>   HC [stage 0] compiler/stage1/build/FiniteMap.o
> compilation IS NOT required
>   HC [stage 0] compiler/stage1/build/Name.o-boot
>
> (then I interrupted it).
>
> Also, in `mk/config.mk` I see this:
> BUILD_SPHINX_HTML= YES
>
> -Iavor
>
>
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Building the docs, again

2017-10-31 Thread Iavor Diatchki
Hello,

sometime ago, I asked if it is possible to build just the GHC docs, without
building the compiler.  I was told to just run `make html`.  This does not
appear to work, the command seems to just start building GHC.  What am I
doing wrong?

Here is the output I see, running the command from the root of the GHC tree.

> make html V=0
===--- building phase 0
make --no-print-directory -f ghc.mk phase=0 phase_0_builds
make[1]: Nothing to be done for 'phase_0_builds'.
===--- building phase 1
make --no-print-directory -f ghc.mk phase=1 phase_1_builds
  HC [stage 0] compiler/stage1/build/BufWrite.o
  HC [stage 0] compiler/stage1/build/Pretty.o
compilation IS NOT required
  HC [stage 0] compiler/stage1/build/PprColour.o
compilation IS NOT required
  HC [stage 0] compiler/stage1/build/Outputable.o
compilation IS NOT required
  HC [stage 0] compiler/stage1/build/Json.o
compilation IS NOT required
  HC [stage 0] compiler/stage1/build/SrcLoc.o
compilation IS NOT required
  HC [stage 0] compiler/stage1/build/BasicTypes.o
compilation IS NOT required
  HC [stage 0] compiler/stage1/build/Unique.o
  HC [stage 0] compiler/stage1/build/Packages.o-boot
compilation IS NOT required
  HC [stage 0] compiler/stage1/build/FiniteMap.o
compilation IS NOT required
  HC [stage 0] compiler/stage1/build/Name.o-boot

(then I interrupted it).

Also, in `mk/config.mk` I see this:
BUILD_SPHINX_HTML= YES

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


Re: A type checker plugin for row types

2017-09-11 Thread Iavor Diatchki
Ah, yes, derived constraints.  The mapping to logic I have in my mind is as
follows:

Given = assumption, used in proofs
Wanted = goal, needs proof
Derived = implied by assumptions and goals

A derived constraint may be used to instantiate touchable unification
variables, and guarantees that in doing so we are not loosing any generally.

Consider, for example, a wanted: `(x + 5) ~ 8`.  From this we can generate
a new derived constraint `x ~ 3`, which would allow GHC to instantiate `x`
to 3.

A derived constraint could also be used to detect that the current set of
goals is inconsistent, for example if we got a derived constraint
equivalent to False, we would immediately know that the current set of
goals has no solution.

-Iavor

On Mon, Sep 11, 2017, 9:35 AM Adam Gundry  wrote:

> Hi Nick,
>
> This is great work, and I look forward to seeing the code once it is
> ready. I've had a quick glance over your wiki page, and thought I should
> send you some initial comments, though it deserves deeper attention
> which I will try to find time to give it. :-)
>
> I don't see a reference to Iavor's paper "Improving Haskell Types with
> SMT" (http://yav.github.io/publications/improving-smt-types.pdf). If
> you've not come across it, it might give a useful alternative
> perspective on how plugins work, especially with regard to derived
> constraints.
>
> The following is based on my faulty memory, so apologies if it is out of
> date or misleading...
>
> > When/where exactly do Derived constraints arise?
>
> Suppose I have a class with an equality superclass
>
> class a ~ b => C a b
>
> and a wanted constraint `C alpha Int`, for some touchable variable
> `alpha`. This leads to a derived constraint `alpha ~ Int` thanks to the
> superclass (derived means we don't actually need evidence for it in
> order to build the core term, but solving it might help fill in some
> touchable variables).  Sorry if this is obvious and not exact enough!
>
> > When do touchables "naturally" arise in Given constraints?
>
> Do you mean "touchable" or "unification variable" here (and elsewhere?).
> A skolem is always untouchable, but the converse is not true.
>
> I think that unification variables can arise in Given constraints, but
> that they will always be untouchable. Suppose we have defined
>
> f :: forall a b . ((a ~ b) => a -> b) -> Int
>
> (never mind that it is ambiguous) and consider type-checking the call `f
> id`. We end up checking `id` against type `a -> b` with given `a ~ b`
> where `a` and `b` are unification variables. They must be untouchable,
> however, otherwise we might unify them, which would be wrong.
>
> Hope this helps,
>
> Adam
>
>
> On 10/09/17 23:24, Nicolas Frisby wrote:
> > Hi all. I've been spending my free time for the last couple months on a
> > type checker plugin for row types. The free time waxes and wanes;
> > sending an email like this one was my primary goal for the past couple
> > weeks.
> >
> > At the very least, I hoped this project would let me finally get some
> > hands on experience with OutsideIn. And I definitely have. But I've also
> > made more progress than I anticipated, and I think the plugin is
> > starting to have legs!
> >
> > I haven't uploaded the code yet to github -- it's not quite ready to
> > share. But I did do a write up on the dev wiki.
> >
> >
> >
> https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain
> >
> > I would really appreciate and questions, comments, and --- boy, oh boy
> > --- answers.
> >
> > I hope to upload within a week or so, and I'll update that wiki page and
> > reply to this email when I do.
> >
> > Thanks very much. -Nick
> >
> > P.S. -- I've CC'd and BCC'd people who I anticipate would be
> > specifically interested in this (e.g. plugins, row types, etc). Please
> > feel free to forward to others that come to mind; I know some inboxes
> > abjectly can't afford default list traffic.
> >
> > P.P.S. -- One hold up for the upload is: which license? I intend to
> > release under BSD3, mainly to match GHC since one ideal scenario would
> > involve being packaged with/integrated into GHC. But my brief recent
> > research suggests that the Apache license might be more conducive to
> > eventual widespread adoption. If you'd be willing to advise or even just
> > refer me to other write ups, please feel free to email me directly or to
> > start a separate thread on a more appropriate distribution list (CC'ing
> > me, please). Thanks again.
>
>
> --
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
> ___
> 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: A type checker plugin for row types

2017-09-11 Thread Iavor Diatchki
Hello Nick,

very nice!  Do you have any thoughts on how to use rows in class/type
family declarations (i.e. how do we match on them)?  For example, if I was
to use the rows to make up some sort of record, system (i.e. declare `Rec
:: Row -> Type`), how might I define the `Show` instance for `Rec`?

-Iavor



On Mon, Sep 11, 2017 at 12:10 AM Ara Adkins  wrote:

> Glad I could be of help! I just gave it a read and that generated core is
> much better than I expected. I’d still have some concerns regarding certain
> uses (e.g. named arguments) having more performance overhead than hoped,
> but at this stage it’s far better than I would’ve initially thought!
>
> Definitely a useful addition to the wiki page.
>
>
> _ara
>
> On 10 Sep 2017, at 23:58, Nicolas Frisby  wrote:
>
> Whoops! I forgot about that section of my draft. I added a little blurb
> ("Performance?") Thanks Ara!
>
>
>
> On Sun, Sep 10, 2017 at 3:41 PM Ara Adkins  wrote:
>
>> Just given this a read!
>>
>> It looks like you’ve put a fantastic amount of effort into this so far,
>> and I can certainly see how it’s finding its legs! I’m very much looking
>> forward to seeing this develop further. I can definitely foresee some uses
>> for polykinded column types, and the possibility for named arguments is
>> certainly interesting (though I have some concerns about performance —
>> though none are relevant at such an early stage).
>>
>> Unfortunately I don’t think I can answer any of the questions that I
>> spotted on my read-through.
>>
>> Again, I’m looking forward to seeing this develop, and the naming of
>> `coxswain` and `sculls` gave me a giggle.
>>
>> _ara
>>
>> On 10 Sep 2017, at 23:24, Nicolas Frisby 
>> wrote:
>>
>> Hi all. I've been spending my free time for the last couple months on a
>> type checker plugin for row types. The free time waxes and wanes; sending
>> an email like this one was my primary goal for the past couple weeks.
>>
>> At the very least, I hoped this project would let me finally get some
>> hands on experience with OutsideIn. And I definitely have. But I've also
>> made more progress than I anticipated, and I think the plugin is starting
>> to have legs!
>>
>> I haven't uploaded the code yet to github -- it's not quite ready to
>> share. But I did do a write up on the dev wiki.
>>
>>
>> https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker/RowTypes/Coxswain
>>
>> I would really appreciate and questions, comments, and --- boy, oh boy
>> --- answers.
>>
>> I hope to upload within a week or so, and I'll update that wiki page and
>> reply to this email when I do.
>>
>> Thanks very much. -Nick
>>
>> P.S. -- I've CC'd and BCC'd people who I anticipate would be specifically
>> interested in this (e.g. plugins, row types, etc). Please feel free to
>> forward to others that come to mind; I know some inboxes abjectly can't
>> afford default list traffic.
>>
>> P.P.S. -- One hold up for the upload is: which license? I intend to
>> release under BSD3, mainly to match GHC since one ideal scenario would
>> involve being packaged with/integrated into GHC. But my brief recent
>> research suggests that the Apache license might be more conducive to
>> eventual widespread adoption. If you'd be willing to advise or even just
>> refer me to other write ups, please feel free to email me directly or to
>> start a separate thread on a more appropriate distribution list (CC'ing me,
>> please). Thanks again.
>>
>> ___
>> 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
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: GHC staus

2017-09-04 Thread Iavor Diatchki
Hello,

Trevor Elliott and I have been slowly working on implementing Simon M's
 "Mutable Constructor Fields" proposal [1].

The current state of the code is here:
https://github.com/yav/ghc/tree/wip/mutable-fields

I am not sure if this would be ready in time for 8.4 as I don't know what
the time-line looks like, and also, the actual proposal is still in the
process of being reviewed by the GHC committee.

-Iavor

[1]
https://github.com/simonmar/ghc-proposals/blob/mutable-fields/proposals/-mutable-fields.rst



On Sun, Sep 3, 2017 at 2:15 PM Simon Peyton Jones via ghc-devs <
ghc-devs@haskell.org> wrote:

> Ben, Simon, and ghc-devs
>
> I have to write slides for the GHC status talk in the Haskell
> Implementor’s meeting.
>
> Usually we have
>
>1. Current status (current release)
>2. What’s cooking for the next release
>3. GHC community comments
>
> As background we have
>
>- Our Apr 17 status page
>
>- Our 8.2 release notes
>
> 
>- Our 8.4 status page
>
>
> What would you put under (1-3)?  Anything you’d like to see highlighted?
>
> Simon
> ___
> 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


Building GHC reference manual?

2017-07-11 Thread Iavor Diatchki
Hello,

is it possible to build just the HTML for the GHC reference manual, without
building the whole of GHC, and if so how do I do it?

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


Re: Problems with `arc` and `phabricator`

2017-01-26 Thread Iavor Diatchki
Ah good, that worked.  I've pushed before, I wonder what happened to my key?

On Thu, Jan 26, 2017 at 1:39 PM, Matthew Pickering <
matthewtpicker...@gmail.com> wrote:

> Hello Iavor,
>
> You need to upload you ssh key to phabricator.
>
> You can do it here,
>
> https://phabricator.haskell.org/settings/user/yav/page/ssh/
>
> If you need any more help with phab then feel free to ping me on IRC
> or by email.
>
> Matt
>
>
> On Thu, Jan 26, 2017 at 9:35 PM, Iavor Diatchki
>  wrote:
> > Hello,
> >
> > I just fixed a small bug in GHC (#11406) and I'm trying to push the
> change
> > to `phabricator` for review, but the command is failing.  Here is my
> output,
> > could you please advise on what to do?
> >
> >> arc diff
> > Linting...
> >  LINT OKAY  No lint problems.
> > Running unit tests...
> > No unit test engine is configured for this project.
> >  PUSH STAGING  Pushing changes to staging area...
> > Permission denied (publickey,keyboard-interactive).
> > fatal: Could not read from remote repository.
> >
> > Please make sure you have the correct access rights
> > and the repository exists.
> >  STAGING FAILED  Unable to push changes to the staging area.
> > Usage Exception: Failed to push changes to staging area. Correct the
> issue,
> > or use --skip-staging to skip this step.
> >
> > Clearly, there is some sort of permission issue...
> >
> > -Iavor
> >
> > ___
> > 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


Problems with `arc` and `phabricator`

2017-01-26 Thread Iavor Diatchki
Hello,

I just fixed a small bug in GHC (#11406) and I'm trying to push the change
to `phabricator` for review, but the command is failing.  Here is my
output, could you please advise on what to do?

> arc diff
Linting...
 LINT OKAY  No lint problems.
Running unit tests...
No unit test engine is configured for this project.
 PUSH STAGING  Pushing changes to staging area...
Permission denied (publickey,keyboard-interactive).
fatal: Could not read from remote repository.

Please make sure you have the correct access rights
and the repository exists.
 STAGING FAILED  Unable to push changes to the staging area.
Usage Exception: Failed to push changes to staging area. Correct the issue,
or use --skip-staging to skip this step.

Clearly, there is some sort of permission issue...

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


Re: `dump-core` a prettier GHC core viewer

2017-01-12 Thread Iavor Diatchki
Hello,

not really, the plugin does not do anything clever---it simply walks over
the GHC core and renders whatever it deems necessary to JSON.  The only
extra bits it does is to make the unique names globally unique (I thought
GHC already did that, but apparently not, perhaps that happens during
tidying?).

I was thinking of trying to do something like this across compilations
(i.e., where you keep a history of all the files to compare how your
changes to the source affected the core), but it hadn't occurred to me to
try to do it for each phase.  Please file a ticket, or even better if you
have the time please feel free to hack on it.  I was just finding myself
staring at a lot of core, and wanted something a little easier to read, but
with all/most of the information still available.

It would be awesome to have a more clever tool that helps further with
these sorts of low level optimizations---at present I find it to be a
rather unpleasant task and so avoid it when I can :-)

-Iavor










On Thu, Jan 12, 2017 at 2:58 PM, Joachim Breitner 
wrote:

> Hi,
>
> Am Donnerstag, den 12.01.2017, 14:18 -0800 schrieb Iavor Diatchki:
> > http://yav.github.io/dump-core/example-output/Galua.OpcodeInterpreter
> > .html
>
> this is amazing! It should in no way sound diminishing if I say that I
> always wanted to create something like that (and I am sure I am not the
> online one who will say that :-)).
>
> Can your tool step forward and backward between dumps from different
> phases, correlating the corresponding entries?
>
> Thanks,
> 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
> ___
> 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: `dump-core` a prettier GHC core viewer

2017-01-12 Thread Iavor Diatchki
Hello,

sorry about the link mix-up, the second one was supposed to be a link to
the GitHub:

https://github.com/yav/dump-core/

The README.md, which is rendered on GitHub, has instructions on how to use
the plugin, and I just updated it with some more information on how to use
the rendered HTML.   You can have a look at a sample rendered module here:

http://yav.github.io/dump-core/example-output/Galua.OpcodeInterpreter.html

The most striking thing everyone seems to notice first is that there are
many variables that have the same name---this is because I am only
rendering the string part of the names, without the uniques.  The hovering
behavior does use the uniques though, so that's what I usually use to
disambiguate the variables.   It would be easy enough to show the numbers
if people would like that.  I am sure that there are many other things that
can be improved---if you have ideas / suggestions, please file an issue on
github.

Cheers,
-Iavor










On Thu, Jan 12, 2017 at 1:23 PM, Simon Peyton Jones 
wrote:

> Iavor
>
>
>
> Sounds good…but there are no instructions on what it does, screen shots,
> why one might want it, how to install, how to use…  Both URLs below are
> the same
>
>
>
> Simon
>
>
>
> *From:* ghc-devs [mailto:ghc-devs-boun...@haskell.org] *On Behalf Of *Iavor
> Diatchki
> *Sent:* 12 January 2017 18:36
> *To:* Haskell Cafe ; ghc-devs@haskell.org
> *Subject:* ANN: `dump-core` a prettier GHC core viewer
>
>
>
> Hello,
>
>
>
> Over the holidays I wrote a small GHC plugin to help me do some low-level
> optimizations of Haskell code.  I thought it might be of use to other
> people too, so please try it out!
>
>
>
> When enabled, the plugin will save the Core generated by GHC in JSON
> format, and also render it in HTML for human inspection.
>
>
>
> The plugin is available on Hackage:
>
> http://hackage.haskell.org/package/dump-core
> <https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fhackage.haskell.org%2Fpackage%2Fdump-core&data=02%7C01%7Csimonpj%40microsoft.com%7C6924b842575e4f63218308d43b19f45e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636198430040472262&sdata=u5N0HOqiy38bvX%2FOC%2BKaEdtdJTYtbQAyxL%2Fvkk2wZ4M%3D&reserved=0>
>
>
>
> The instructions on how to use it are in the README file.
>
> You may also read about it at the github page:
>
> http://hackage.haskell.org/package/dump-core
> <https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fhackage.haskell.org%2Fpackage%2Fdump-core&data=02%7C01%7Csimonpj%40microsoft.com%7C6924b842575e4f63218308d43b19f45e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636198430040472262&sdata=u5N0HOqiy38bvX%2FOC%2BKaEdtdJTYtbQAyxL%2Fvkk2wZ4M%3D&reserved=0>
>
>
>
> There are many things that could probably be improved, just let me know.
> Also, if you are good at design, I could use some help making things look
> prettier :)
>
>
>
> Happy hacking,
>
> -Iavor
>
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


ANN: `dump-core` a prettier GHC core viewer

2017-01-12 Thread Iavor Diatchki
Hello,

Over the holidays I wrote a small GHC plugin to help me do some low-level
optimizations of Haskell code.  I thought it might be of use to other
people too, so please try it out!

When enabled, the plugin will save the Core generated by GHC in JSON
format, and also render it in HTML for human inspection.

The plugin is available on Hackage:
http://hackage.haskell.org/package/dump-core

The instructions on how to use it are in the README file.
You may also read about it at the github page:
http://hackage.haskell.org/package/dump-core

There are many things that could probably be improved, just let me know.
Also, if you are good at design, I could use some help making things look
prettier :)

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


Semantics of MVars and IORefs?

2016-10-21 Thread Iavor Diatchki
Hello,

recently, I and a few colleagues have been wondering about the interaction
between IORefs and MVars, and we can't seem to find any explicit
documentation stating the behavior, so I was wondering if anyone might know
the answer.

The question is:  is it safe to use IORefs in a multi-threaded program,
provided that the uses are within a "critical section" implemented with
MVars.  Here is a simple program to illustrate the situation: we have two
threads, each thread takes a lock, increments a counter, then releases the
lock:

> import Control.Concurrent
> import Data.IORef
>
> main :: IO ()
> main =
>   do lock<- newMVar ()
>  counter <- newIORef 0
>  forkIO (thread lock counter)
>  thread lock counter
>
> thread :: MVar () -> IORef Integer -> IO a
> thread lock counter =
>   do takeMVar lock
>  value <- readIORef counter
>  print value
>  writeIORef counter (value + 1)
>  putMVar lock ()
>  thread lock counter

The question is if this program has a race condition or not, due to the use
of IORefs?  More explicitly, the concern is if a write to an IORef in one
thread is guaranteed to be seen by a read from the same IORef in another
thread, provided that there is proper synchronization between the two.

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


Re: qualified module export

2016-10-11 Thread Iavor Diatchki
Hello,

There may be some more thinking to be done on the design of this feature.
In particular, if a module `M` has en export declaration `module T`, this
is not at all the same as adding `import T` in modules exporting `M`.  The
reason is that meaning of `module T` depends on what is in scope in `M` and
with what names.For example:
   * `module T` may export only some of the names from `T` (e.g. if `M`
contains `import T(onlyThisName)`); or,
   * `module T` may export the names from an entirely different module
(e.g., if `M` contains `import S as T`); or,
   * `module T` may export a combination of multiple modules (e.g., if `M`
contains `import S1 as T` and `import S2 as T`).

So, I would expect an export of the form `qualified module T as X` to work
in a similar fashion (for the full details on the current semantics you
could have a look at [1]).

The next issue would be that, currently, entities exported by a module are
only identified by an unqualified name, and the imports introduce qualified
names as necessary.  It might make sense to allow modules to also export
qualified names instead, but then we'd have to decide what happens on the
importing end.  Presumably, a simple `import M` would now bring both some
qualified and some unqualified names.  This means that the explicit import
and hiding lists would have to support qualified names, seems doable.
However, we'd also have to decide how `import M as X` works, in particular
how does it affect imported qualified names.  One option would be to have
`X` replace the qualifier, so if `A.b` is imported via `import M as X`, the
resulting name would be `X.b`.  Another option would be to have `X` extend
the qualifier, so `A.b` would become `X.A.b` locally.  Neither seems
perfect:  the first one is somewhat surprising, where you might
accidentally "overwrite" a qualifier and introduce name conflicts; the
second does not allow exported qualified names to ever get shorter.

I hope this is helpful,
-Iavor

[1] http://yav.github.io/publications/modules98.pdf


On Tue, Oct 11, 2016 at 8:54 AM, Karl Cronburg  wrote:

> Hello,
>
> I'm attempting to add support for export of qualified modules (feature
> request #8043), and any guidance would be greatly appreciated. Namely I'm
> very familiar with languages / grammars / happy and was easily able to add
> an appropriate production alternative to Parser.y to construct a new AST
> node when 'qualified module' is seen in the export list, i.e.:
>
> |  'module' modid {% amsu (sLL $1 $> (IEModuleContents $2))
>   [mj AnnModule $1] }
> |  'qualified' 'module' qconid --maybeas
>   {% amsu (sLL $2 $> (IEModuleQualified $3))
>   [mj AnnQualified $1] }
>
> But now I'm lost in the compiler internals. Where should I be looking /
> focusing on? In particular:
>
> - Where do exported identifiers get added to the list of "[LIE Name]" in
> ExportAccum (in TcRnExports.hs)?
>
> Thanks,
> -Karl Cronburg-
>
> ___
> 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: Allow top-level shadowing for imported names?

2016-10-03 Thread Iavor Diatchki
Hi,

Lennart suggested that some time ago, here is the thread from the last time
we discussed it:

https://mail.haskell.org/pipermail/haskell-prime/2012-July/003702.html

I think it is a good plan!

-Iavor



On Mon, Oct 3, 2016 at 4:46 AM, Richard Eisenberg 
wrote:

> By all means make the proposal -- I like this idea.
>
> > On Oct 3, 2016, at 4:29 AM, Herbert Valerio Riedel 
> wrote:
> >
> > Hi *,
> >
> > I seem to recall this was already suggested in the past, but I can't
> > seem to find it in the archives. For simplicity I'll restate the idea:
> >
> >
> >foo :: Int -> Int -> (Int,Int)
> >foo x y = (bar x, bar y)
> >  where
> >bar x = x+x
> >
> > results merely in a name-shadowing warning (for -Wall):
> >
> >foo.hs:4:9: warning: [-Wname-shadowing]
> >This binding for ‘x’ shadows the existing binding
> >  bound at foo.hs:2:5
> >
> >
> > However,
> >
> >import Data.Monoid
> >
> >(<>) :: String -> String -> String
> >(<>) = (++)
> >
> >main :: IO ()
> >main = putStrLn ("Hi" <> "There")
> >
> > doesn't allow to shadow (<>), but rather complains about ambiguity:
> >
> >bar.hs:7:23: error:
> >Ambiguous occurrence ‘<>’
> >It could refer to either ‘Data.Monoid.<>’,
> > imported from ‘Data.Monoid’ at
> bar.hs:1:1-18
> >  or ‘Main.<>’, defined at bar.hs:4:1
> >
> >
> > This is of course in line with the Haskell Report, which says in
> > https://www.haskell.org/onlinereport/haskell2010/
> haskellch5.html#x11-1010005.3
> >
> > | The entities exported by a module may be brought into scope in another
> > | module with an import declaration at the beginning of the module. The
> > | import declaration names the module to be imported and optionally
> > | specifies the entities to be imported. A single module may be imported
> > | by more than one import declaration. Imported names serve as top level
> > | declarations: they scope over the entire body of the module but may be
> > | shadowed by *local non-top-level bindings.*
> >
> >
> > However, why don't we allow this to be relaxed via a new language
> > extensions, to allow top-level bindings to shadow imported names (and
> > of course emit a warning)?
> >
> > Unless I'm missing something, this would help to keep existing and
> > working code compiling if new versions of libraries start exporting new
> > symbols (which happen to clash with local top-level defs), rather than
> > resulting in a fatal name-clash; and have no major downsides.
> >
> > If this sounds like a good idea, I'll happily promote this into a proper
> > proposal over at https://github.com/ghc-proposals/ghc-proposals; I
> > mostly wanted to get early feedback here (and possibly find out if and
> > where this was proposed before), before investing more time turning
> > this into a fully fledged GHC proposal.
> >
> > Cheers,
> >  HVR
> > ___
> > 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
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Last call for merge requests for 8.0.2

2016-08-29 Thread Iavor Diatchki
Hello,

I don't have a patch, but I think that #12433 is a really serious bug that
deserves a timely fix, as compiling with `-dynamic` on Linux produces code
that runs but produces incorrect results.
Unfortunately, I don't have time to look into it, and the bug is not in a
part of the compiler I have experience with.

-Iavor

On Mon, Aug 29, 2016 at 2:02 PM, Facundo Domínguez <
facundo.doming...@tweag.io> wrote:

> Hello Ben,
>
>   Could we have these patches added?
>
> http://git.haskell.org/ghc.git/commit/56f47d4a4e418235285d8b8cfe23bd
> e6473f17fc
> http://git.haskell.org/ghc.git/commit/567dbd9bcb602accf3184b83050f29
> 82cbb7758b
>
> These allow reify to reach local variables when used with addModFinalizer.
>
> Best,
> Facundo
>
> On Mon, Aug 29, 2016 at 4:00 PM, Ben Gamari  wrote:
> > tl;dr. GHC 8.0.2 is coming. If you have a fix which you'd like to see
> >merged into 8.0.2 and isn't already present in the tree, please
> >speak up!
> >
> >
> > Hello everyone,
> >
> > Over the last week I have been working down the (rather long) merge
> > queue for the ghc-8.0 branch in preparation for a 8.0.2 release. At this
> > point I think have merged nearly everything which will likely make it in
> > to 8.0.2.
> >
> > If you have a patch which hasn't made it to the ghc-8.0 branch that you
> > would like to see merged, please raise your concern on the appropriate
> > Trac ticket.
> >
> > Thanks!
> >
> > - 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
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Question about initializing the run-time system

2016-08-15 Thread Iavor Diatchki
Hello,

GHC's user guide says that the run-time system cannot re-initialize itself,
after it was shut-down (i.e., you can't call `hs_init` after calling
`hs_exit`).

Could anyone shed some light on why that is?

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


Re: Proposal process status

2016-07-20 Thread Iavor Diatchki
Hello Ben,

I posted this when you originally asked for feed-back, but perhaps it
got buried among the rest of the e-mails.

I think the proposal sounds fairly reasonable, but it is hard to say how
well it will work in practice until we try it, and we should be ready to
change it if needs be.

Some clarifying questions on the intended process:
   1.  After submitting the initial merge request, is the person making the
proposal to wait for any kind of acknowledgment, or just move on to step 2?
   2. Is the discussion going to happen on one of the mailing lists, if so
which?   Is it the job of the proposing person to involve/notify the
committee about the discussion?  If so, how are they to find out who is on
the committee?
   3. How does one actually perform step 3, another pull request or simply
an e-mail to someone?

Typo: two separate bullets in the proposal are labelled as 4.

Cheers,
-Iavor

On Wed, Jul 20, 2016 at 2:36 AM, Ben Gamari  wrote:

>
> Hello everyone,
>
> As you hopefully know, a few weeks ago we proposed a new process [1] for
> collecting, discussing, and deciding upon changes to GHC and its Haskell
> superset. While we have been happy to see a small contingent of
> contributors join the discussion, the number is significantly smaller
> than the set who took part in the earlier Reddit discussions.
>
> In light of this, we are left a bit uncertain of how to proceed. So,
> we would like to ask you to let us know your feelings regarding the
> proposed process:
>
>   * Do you feel the proposed process is an improvement over the status
> quo?
>
>   * Why? (this needn't be long, just a sentence hitting the major points)
>
>   * What would you like to see changed in the proposed process, if
> anything?
>
> That's all. Again, feel free to reply either on the GitHub pull request
> [1] or this thread if you would prefer. Your response needn't be long;
> we just want to get a sense of how much of the community feels that 1)
> this effort is worth undertaking, and 2) that the proposal before us is
> in fact an improvement over the current state of affairs.
>
> Thanks for your help!
>
> Cheers,
>
> - Ben
>
>
> [1] https://github.com/ghc-proposals/ghc-proposals/pull/1
>
> ___
> Glasgow-haskell-users mailing list
> glasgow-haskell-us...@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Rethinking GHC's approach to managing proposals

2016-07-11 Thread Iavor Diatchki
Hello,

I think this sounds fairly reasonable, but it is hard to say how well it
will work in practice until we try it.

Some clarifying questions on the intended process:
   1.  After submitting the initial merge request, is the person making the
proposal to wait for any kind of acknowledgment, or just move on to step 2?
   2. Is the discussion going to happen on one of the mailing lists, if so
which?   Is it the job of the proposing person to involve/notify the
committee about the discussion?  If so, how are they to find out who is on
the committee?
   3. How does one actually perform step 3, another pull request or simply
an e-mail to someone?

Typo: two separate bullets in the proposal are labelled as 4.

Cheers,
-Iavor







On Mon, Jul 11, 2016 at 2:36 PM, Simon Peyton Jones via
Glasgow-haskell-users  wrote:

> Just to be clear:
>
> * We are actively seeking feedback about the proposal [4] below.
>   It's not a fait-accompli.
>
> * You can join the dialogue by (a) replying to this email,
>   (b) via the "Conversations" tab of [4], namely
>   https://github.com/ghc-proposals/ghc-proposals/pull/1
>   Doubtless via reddit too!
>
>   If you don't like something, the more specific and concrete you
>   can be about a better alternative, the better.  E.g. Richard's
>   comments on the "conversations" tab both ask questions and propose
>   answers.  Bravo!
>
> Simon
>
> | -Original Message-
> | From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Ben
> | Gamari
> | Sent: 09 July 2016 21:46
> | To: GHC developers ; ghc-users  | us...@haskell.org>
> | Subject: Rethinking GHC's approach to managing proposals
> |
> | Hello everyone,
> |
> | Recently there has been a fair bit of discussion[1,2] around the
> | mechanisms by which proposed changes to GHC are evaluated. While we have
> | something of a formal proposal protocol [3], it is not clearly
> | documented, inconsistently applied, and may be failing to serve a
> | significant fraction of GHC's potential contributor pool.
> |
> | Over the last few weeks, I have been doing a fair amount of reading,
> | thinking, and discussing to try to piece together a proposal scheme
> | which better serves our community.
> |
> | The resulting proposal [4] is strongly inspired by the RFC process in
> | place in the Rust community [5], the leaders of which have thought quite
> | hard about fostering community growth and participation. While no
> | process is perfect, I feel like the Rust process is a good starting
> | point for discussion, offering enough structure to guide new
> | contributors through the process while requiring only a modest
> | investment of developer time.
> |
> | To get a sense for how well this will work in our community, I propose
> | that we attempt to self-host the proposed process. To this end I have
> | setup a ghc-proposals repository [6] and opened a pull request for
> | discussion of the process proposal [4].
> |
> | Let's see how this goes.
> |
> | Cheers,
> |
> | - Ben
> |
> |
> | [1]
> | https://na01.safelinks.protection.outlook.com/?url=https%3a%2f%2fwww.red
> | dit.com%2fr%2fhaskell%2fcomments%2f4oyxo2%2fblog_contributing_to_ghc%2f&
> | data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c99735311c5f64cac6a6608
> | d3a83a032a%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=Hl6GqRWfu7IOQtpE
> | jpfsNAkv3mmLgNKm2ciQDoMe6HA%3d
> | [2]
> | https://na01.safelinks.protection.outlook.com/?url=https%3a%2f%2fwww.red
> | dit.com%2fr%2fhaskell%2fcomments%2f4isua9%2fghc_development_outsidein%2f
> | &data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7c99735311c5f64cac6a660
> | 8d3a83a032a%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=bj2AQqQirX3X%2f
> | 4%2fFr05eXFuD4yW0r9Nmrmdg7IGEF%2f8%3d
> | [3]
> | https://ghc.haskell.org/trac/ghc/wiki/WorkingConventions/AddingFeatures
> | [4] https://github.com/ghc-proposals/ghc-
> | proposals/pull/1/files?short_path=14d66cd#diff-
> | 14d66cda32248456a5f223b6333c6132
> | [5] https://github.com/rust-lang/rfcs
> | [6] https://github.com/ghc-proposals/ghc-proposals
> ___
> Glasgow-haskell-users mailing list
> glasgow-haskell-us...@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


GHC nightly builds?

2016-05-02 Thread Iavor Diatchki
Hello,

do we have nightly builds for development versions of GHC somewhere?

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


Re: Bikeshedding request for GHCi's :type

2016-04-28 Thread Iavor Diatchki
Currently GHCi shows the "real" type of an expression (i.e., the inferred
generalized type), when you ask it:

Prelude> :t 1
1 :: Num a => a

Note that there is no defaulting happening, at least at the top level---of
course if there were local things that needed to be defaulted while the
expression was being type-checked then those would be defaulted.

If you ask GHCi to *evaluate* a polymorphic expression, then it will try to
default the type when it is figuring out how to show the result.  The
alternative would be to say "sorry, I can't evaluate this, because it is
polymorphic, so please tell me what type do you mean".  This is probably a
bit too inconvenient for practical use.

-Iavor




On Thu, Apr 28, 2016 at 5:24 AM, Johannes Waldmann <
johannes.waldm...@htwk-leipzig.de> wrote:

> > .. :type should report the real type
>
> What about defaulting? Is it real?
> https://ghc.haskell.org/trac/ghc/ticket/11994
>
> - J.W.
> ___
> 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: Custom Type Error not getting triggered in the nested Type function call

2016-04-27 Thread Iavor Diatchki
Hi,

yes, this looks like a bug.  Could you please file a report on the
bug-tracker?

-Iavor

On Wed, Apr 27, 2016 at 9:43 AM, Magesh B  wrote:

> Hello,
>
> I have partial type function which is invoked by another type function.
> When the inner type function fails with TypeError, outer type function is
> not been able to propagate that type error to its caller.
> As a result of it, I'm getting following error
>   • No instance for (KnownSymbol (NestedPartialTF (TypeError ...)))
>  instead of
>   • Unexpected type @ NestedPartialTF: Char
>
> Is this a bug? This behavior seems bit counter-intuitive as to work
> around, I had to write another (duplicate) type function at the top level
> to get the desired type error
>
> I'm using GHC-8 RC 3 and have attached complete src for reference.
>
> Regards,
> Magesh B
>
> ___
> 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: Bikeshedding request for GHCi's :type

2016-04-27 Thread Iavor Diatchki
Hello Richard,

I think that `:type` should report the real type of an expressions (i.e.,
the fully generalized inferred type, just like it does now).  Certainly I
wouldn't want `:type` to show me some kind of (more or less) arbitrary
specialization of the type.

It could be useful to have a ghci command that would show all
instantiations of a class method (just 1 level deep) using the instances
that are currently in scope.  This would be essentially a combination of
`:info` on a class and a method.  For example, this is what it would look
like on some of the methods in 7.10's Prelude:

:inst length
length :: [a] -> Int
length :: Maybe a -> Int
length :: Either a b -> Int
length :: (a,b) -> Int

:inst (==)
(==) :: Integer -> Integer -> Bool
(==) :: Word -> Word -> Bool
...
(==) :: Eq a => [a] -> [a] -> Bool-- Note that we only instantiate the
outer class
...
(==) :: (Eq a, Eq b, Eq c) => (a,b,c) -> (a,b,c) -> Bool  -- ditto

:inst mapM
mapM :: Monad m => (a -> m b) -> [a] -> m [b]
mapM :: Monad m => (a -> m b) -> Maybe a -> m (Maybe b)
mapM :: Monad m => (a -> m b) -> Either e a -> m (Either e b)
mapM :: Monad m => (a -> m b) -> (e,a) -> m (e,b)

This could be generalized to expressions, rather than just methods, but for
expressions with multiple constraints one could get an explosion of
possible instantiations.  However, it would be quite cool to allow things
like this:

:inst 1
1 :: Word
1 :: Integer
1 :: Int
1 :: Float
1 :: Double

Anyway, just some ideas.

-Iavor




















On Wed, Apr 27, 2016 at 8:16 AM, Manuel Gómez  wrote:

> On Wed, Apr 27, 2016 at 10:15 AM, John Leo  wrote:
> > Speaking as someone teaching his coworkers Haskell now, Eric's is the
> best
> > suggestion I've seen so far.
> >
> > What I like about it:
> > * The original meaning of :type is unchanged.
> > * No new command is added (I prefer adding a flag to adding another
> > command).
> > * With the flag on, the full type is shown along with the possible
> > specializations (and good to note the list might not be exhaustive).
> This
> > way, beginners can still see what the type should look like even if they
> > want to ignore it for now.  This is similar to learning to read Japanese
> by
> > using furigana.  It may be a bit confusing for beginners at first, but I
> > expect they'll quickly learn to ignore it until they need it, and I
> agree it
> > will be useful for experienced Haskellers.
>
> Perhaps a pleasant solution would be to borrow a convention from the
> PostgreSQL community's interactive console psql and its meta-commands:
>
> http://www.postgresql.org/docs/current/static/app-psql.html#APP-PSQL-META-COMMANDS
>
> For example:
>
> > \d[S+] [ pattern ]
> >
> > For each [object] matching the pattern, show all columns, their types,
> the tablespace (if not the default) and any special attributes such as NOT
> NULL or defaults. […]  The command form \d+ is identical, except that more
> information is displayed: any comments associated with the columns of the
> table are shown, as is the presence of OIDs in the table, the view
> definition if the relation is a view, a non-default replica identitysetting.
>
> Many psql commands use this convention: add a + to the end of the
> command, and you get extra information.  It’s quite nmemonic.
> ___
> 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: GHC 8 and Template Haskell

2016-04-15 Thread Iavor Diatchki
I left the "instanceD" functions as is, and added a new function
`instanceWithOverlapD` to avoid that problem:

instanceD :: CxtQ -> TypeQ -> [DecQ] -> DecQ
instanceWithOverlapD :: Maybe Overlap -> CxtQ -> TypeQ -> [DecQ] -> DecQ

The patch is here btw:

https://phabricator.haskell.org/D2118





On Fri, Apr 15, 2016 at 7:14 AM, Ryan Scott  wrote:

> > I've done a quick grep for InstanceD over the stackage-nightly-subset of
> Hackage:
>
> Wouldn't we also need to check for the instanceD function from
> Language.Haskell.TH.Lib as well? I know several of my packages use
> that exclusively over the InstanceD constructor, and I imagine others
> do as well.
>
> Ryan S.
> ___
> Libraries mailing list
> librar...@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: GHC 8 and Template Haskell

2016-04-14 Thread Iavor Diatchki
Sure, I'd be happy to help whoever needs help---just let me know.

The change that one would have to do is:  whenever you'd used "InstaceD"
 replace it with "InstanceD Nothing".




On Thu, Apr 14, 2016 at 2:33 PM, Herbert Valerio Riedel 
wrote:

> On 2016-04-14 at 23:11:26 +0200, Iavor Diatchki wrote:
>
> [...]
>
> > If we were to delay things, we would ship a version of the library that
> has
> > missing functionality *and* we'll break everyone's code on the next
> > release.
>
> >   If we make the change now, then at least when people fix their TH
> > code to work with GHC 8, they'd be getting access to more
> > functionality.
> >
> > This change does indeed change the data structure for declarations, so if
> > you were working with it directly, indeed you'll have to make changes.
>
> This so late in the process involves retroactively tighten upper bounds
> on template-haskell for existing releases on Hackage which already
> extended support to template-haskell-2.11.
>
> Sadly, I have lost track of how many packages were already updated
> several weeks ago since the first RC came out to work with
> template-haskell-2.11 so I don't have any numbers to offer nor a
> concrete list of which packages are likely candidates to become
> penalized for having been early adopters of GHC 8.0.
>
> So this will cause a regression on Hackage which will be actionable only
> after GHC 8.0 final gets out (unless we happen to have a RC4), as
> otherwise we'd break parts of Hackage for GHC 8.0 RC3 users
> (this includes Travis jobs already including GHC 8.0 in their configs)
>
> However, I do sympathize with the desire to get this in while it's still
> relatively cheap, rather than have to wait a year until it's time for
> template-haskell-2.12 ...
>
> Would you be willing to help out with making sure popular packages
> depending on template-haskell[1] are brought up speed as soon as your
> proposed change lands to reduce the pain/cost of such a last-minute
> change?
>
>
>  [1]: http://packdeps.haskellers.com/reverse/template-haskell
>
>
> > However, if you use the "smart" constructors in TH, you shouldn't need to
> > change anything.
> > In particular, I left `instanceD` as before---it does not add any
> > overlapping pragmas, and I added a new function `instanceWithOverlapD`,
> > which has an extra parameter that allows you to specify pragmas.
> >
> > I'd like to get this in, if possible, as I have a library that needs this
> > feature.  My current work-around it quite ugly:  ask the clients of the
> > library to enable "Language OverlappingInstaces", which is cumbersome,
> > *and* generates deprecation warnings.
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: GHC 8 and Template Haskell

2016-04-14 Thread Iavor Diatchki
Hi,

objection!  :-)

If we were to delay things, we would ship a version of the library that has
missing functionality *and* we'll break everyone's code on the next
release.   If we make the change now, then at least when people fix their
TH code to work with GHC 8, they'd be getting access to more functionality.

This change does indeed change the data structure for declarations, so if
you were working with it directly, indeed you'll have to make changes.
However, if you use the "smart" constructors in TH, you shouldn't need to
change anything.
In particular, I left `instanceD` as before---it does not add any
overlapping pragmas, and I added a new function `instanceWithOverlapD`,
which has an extra parameter that allows you to specify pragmas.

I'd like to get this in, if possible, as I have a library that needs this
feature.  My current work-around it quite ugly:  ask the clients of the
library to enable "Language OverlappingInstaces", which is cumbersome,
*and* generates deprecation warnings.

-Iavor






On Thu, Apr 14, 2016 at 1:59 PM, Richard Eisenberg 
wrote:

> I'm happy to be overruled on this, but I vote against this change for GHC
> 8. Personally, I like to have a policy of "no TH changes after the first
> RC". This gives ample time for TH clients to update their code. Iavor's
> suggestion would likely involve a new part of the InstanceD constructor,
> which would affect anyone constructing or matching on this constructor. If
> the change involved, say, only adding new functionality without changing
> anything existing, I would be more willing to include for GHC 8.
>
> And, yes, I agree with Austin.
>
> Richard
>
> On Apr 14, 2016, at 2:17 PM, Austin Seipp  wrote:
>
> > Here's a question, on top of this one: why don't we require
> > template-haskell changes for most corresponding syntax changes? We
> > tend to play catch up with template-haskell sometimes and it's
> > relatively strange. I mean, in some sense, we could have said a while
> > back "This needs another revision, please add template haskell
> > support" and avoided it all.
> >
> > Richard has a better insight into this than I do, I'm sure, but it
> > seems - to me, anyway - like template-haskell support is a reasonable
> > bar for most surface-level syntax change to cross, before getting
> > merged.
> >
> > My intuition tells me that, most of the time, a lot of us simply
> > forget to make the changes, or ask for them in reviews, and so it
> > goes.
> >
> > On Thu, Apr 14, 2016 at 1:12 PM, Ben Gamari  wrote:
> >> Iavor Diatchki  writes:
> >>
> >>> Hello,
> >>>
> >>> Now that "OVERLAPPING" and "OVERLAPPABLE" are pragmas on the
> instances, do
> >>> we have a way to generate instances with such pragmas using Template
> >>> Haskell?   I can't seem to find a way to do this, which is unfortunate.
> >>>
> >>> If I am not missing anything, would there be objections to adding it
> to the
> >>> TH library before the next release---I would volunteer to do the change
> >>> ASAP.
> >>>
> >> Indeed this is an unfortunate gap. Given that this shouldn't be a
> >> terribly invasive change I would be alright with this if Richard
> approves.
> >>
> >> Cheers,
> >>
> >> - Ben
> >>
> >>
> >> ___
> >> Libraries mailing list
> >> librar...@haskell.org
> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> >>
> >
> >
> >
> > --
> > Regards,
> >
> > Austin Seipp, Haskell Consultant
> > Well-Typed LLP, http://www.well-typed.com/
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


GHC 8 and Template Haskell

2016-04-14 Thread Iavor Diatchki
Hello,

Now that "OVERLAPPING" and "OVERLAPPABLE" are pragmas on the instances, do
we have a way to generate instances with such pragmas using Template
Haskell?   I can't seem to find a way to do this, which is unfortunate.

If I am not missing anything, would there be objections to adding it to the
TH library before the next release---I would volunteer to do the change
ASAP.

Let me know,

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


Re: GADTs and functional dependencies?

2016-03-01 Thread Iavor Diatchki
The method `f` of the class is not important---I simplified the example I'd
written before and forgot to delete it.  Apologies for the noise!

On Tue, Mar 1, 2016 at 10:47 AM, Iavor Diatchki 
wrote:

> Hello Conal,
>
> the implementation of fun-deps in GHC is quite limited, and they don't do
> what you'd expect with existential types (like in your example),
> type-signatures, or GADTs.   Basically, GHC only uses fun-deps to fill-in
> types for unification variables, but it won't use them to reason about
> quantified variables.
>
> Here is an example that shows the problem, just using type signatures:
>
> > class F a b | a -> b where
> >   f :: a -> b -> ()
> >
> > instance F Bool Char where
> >  f _ _ = ()
> >
> > test :: F Bool a => a -> Char
> > test a = a
>
> GHC rejects the declaration for `test` because there it needs to prove
> that `a ~ Char`.  Using the theory of fun-deps, the equality follows
> because from the fun-dep we know that:
>
> forall x y z. (F x y, F x z) => (y ~ z)
>
> Now, if we instantiate this axiom with `Bool`, `Char`, and `a`, we can
> prove that `Char ~ a` by combining the instance and the local assumption
> from the signature.
>
> Unfortunately, this is exactly the kind of reasoning GHC does not do.   I
> am not 100% sure on why not, but at present GHC will basically do all the
> work to ensure that the fun-dep axiom for each class is valid (that's all
> the checking that instances are consistent with their fun-deps), but then
> it won't use that invariant when solving equalities.
>
> I hope this helps!
> -Iavor
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
> On Tue, Mar 1, 2016 at 9:38 AM, Conal Elliott  wrote:
>
>> Do GADTs and functional dependencies get along? I'm wondering why the
>> following code doesn't type-check under GHC 7.10.3 and 8.1.20160224:
>>
>> > {-# OPTIONS_GHC -Wall #-}
>> > {-# LANGUAGE GADTs, KindSignatures, MultiParamTypeClasses,
>> FunctionalDependencies #-}
>> >
>> > module FundepGadt where
>> >
>> > class C a b | a -> b
>> >
>> > data G :: * -> * where
>> >   -- ...
>> >   GC :: C a b => G b -> G a
>> >
>> > instance Eq (G a) where
>> >   -- ...
>> >   GC b  == GC b' = b == b'
>>
>> Error message:
>>
>> FundepGadt.hs:14:25: error:
>> • Couldn't match type 'b1’ with 'b’
>>   'b1’ is a rigid type variable bound by
>> a pattern with constructor: GC :: forall a b. C a b => G b ->
>> G a,
>> in an equation for '==’
>> at FundepGadt.hs:14:12
>>   'b’ is a rigid type variable bound by
>> a pattern with constructor: GC :: forall a b. C a b => G b ->
>> G a,
>> in an equation for '==’
>> at FundepGadt.hs:14:3
>>   Expected type: G b
>> Actual type: G b1
>> • In the second argument of '(==)’, namely 'b'’
>>   In the expression: b == b'
>>   In an equation for '==’: (GC b) == (GC b') = b == b'
>> • Relevant bindings include
>> b' :: G b1 (bound at FundepGadt.hs:14:15)
>> b :: G b (bound at FundepGadt.hs:14:6)
>>
>> I think the functional dependency does ensure that "b == b" is
>> well-typed.
>>
>> In contrast, the following type-family version does type-check:
>>
>> > {-# OPTIONS_GHC -Wall #-}
>> > {-# LANGUAGE GADTs, KindSignatures, TypeFamilies #-}
>> >
>> > module TyfamGadt where
>> >
>> > class C a where
>> >   type B a
>> >
>> > data G :: * -> * where
>> >   -- ...
>> >   GC :: C a => G (B a) -> G a
>> >
>> > instance Eq (G a) where
>> >   -- ...
>> >   GC b  == GC b' = b == b'
>>
>> Thanks, - Conal
>>
>> ___
>> ghc-tickets mailing list
>> ghc-tick...@haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
>>
>>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: GADTs and functional dependencies?

2016-03-01 Thread Iavor Diatchki
Hello Conal,

the implementation of fun-deps in GHC is quite limited, and they don't do
what you'd expect with existential types (like in your example),
type-signatures, or GADTs.   Basically, GHC only uses fun-deps to fill-in
types for unification variables, but it won't use them to reason about
quantified variables.

Here is an example that shows the problem, just using type signatures:

> class F a b | a -> b where
>   f :: a -> b -> ()
>
> instance F Bool Char where
>  f _ _ = ()
>
> test :: F Bool a => a -> Char
> test a = a

GHC rejects the declaration for `test` because there it needs to prove that
`a ~ Char`.  Using the theory of fun-deps, the equality follows because
from the fun-dep we know that:

forall x y z. (F x y, F x z) => (y ~ z)

Now, if we instantiate this axiom with `Bool`, `Char`, and `a`, we can
prove that `Char ~ a` by combining the instance and the local assumption
from the signature.

Unfortunately, this is exactly the kind of reasoning GHC does not do.   I
am not 100% sure on why not, but at present GHC will basically do all the
work to ensure that the fun-dep axiom for each class is valid (that's all
the checking that instances are consistent with their fun-deps), but then
it won't use that invariant when solving equalities.

I hope this helps!
-Iavor























On Tue, Mar 1, 2016 at 9:38 AM, Conal Elliott  wrote:

> Do GADTs and functional dependencies get along? I'm wondering why the
> following code doesn't type-check under GHC 7.10.3 and 8.1.20160224:
>
> > {-# OPTIONS_GHC -Wall #-}
> > {-# LANGUAGE GADTs, KindSignatures, MultiParamTypeClasses,
> FunctionalDependencies #-}
> >
> > module FundepGadt where
> >
> > class C a b | a -> b
> >
> > data G :: * -> * where
> >   -- ...
> >   GC :: C a b => G b -> G a
> >
> > instance Eq (G a) where
> >   -- ...
> >   GC b  == GC b' = b == b'
>
> Error message:
>
> FundepGadt.hs:14:25: error:
> • Couldn't match type 'b1’ with 'b’
>   'b1’ is a rigid type variable bound by
> a pattern with constructor: GC :: forall a b. C a b => G b ->
> G a,
> in an equation for '==’
> at FundepGadt.hs:14:12
>   'b’ is a rigid type variable bound by
> a pattern with constructor: GC :: forall a b. C a b => G b ->
> G a,
> in an equation for '==’
> at FundepGadt.hs:14:3
>   Expected type: G b
> Actual type: G b1
> • In the second argument of '(==)’, namely 'b'’
>   In the expression: b == b'
>   In an equation for '==’: (GC b) == (GC b') = b == b'
> • Relevant bindings include
> b' :: G b1 (bound at FundepGadt.hs:14:15)
> b :: G b (bound at FundepGadt.hs:14:6)
>
> I think the functional dependency does ensure that "b == b" is well-typed.
>
> In contrast, the following type-family version does type-check:
>
> > {-# OPTIONS_GHC -Wall #-}
> > {-# LANGUAGE GADTs, KindSignatures, TypeFamilies #-}
> >
> > module TyfamGadt where
> >
> > class C a where
> >   type B a
> >
> > data G :: * -> * where
> >   -- ...
> >   GC :: C a => G (B a) -> G a
> >
> > instance Eq (G a) where
> >   -- ...
> >   GC b  == GC b' = b == b'
>
> Thanks, - Conal
>
> ___
> ghc-tickets mailing list
> ghc-tick...@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: New type of ($) operator in GHC 8.0 is problematic

2016-02-04 Thread Iavor Diatchki
Hello,

how about we simply use two operators:
  1. ($) which only works for standard types (i.e., not #), which we can
use 99% of the time, and
  2. some other operator which has the levity polymorphic type and would be
used in the advanced cases when you are working with unboxed values, etc.
Personally, I use unboxed values rarely enough, that I'd even be OK simply
using parens or naming the sub-expression instead of using $


-Iavor



On Thu, Feb 4, 2016 at 5:38 PM, Christopher Allen  wrote:

> The sort of pragma you suggest would satisfy me. Pragmas like this don't
> bother me and make my job a fair bit easier. Too many, "don't worry about
> this; later" is exhausting. Too many, "don't worry about this; we're not
> even going to have time to cover it" is demoralizing.
>
> On Thu, Feb 4, 2016 at 5:31 PM, Edward Z. Yang  wrote:
>
>> I'm not really sure how you would change the type of 'id' based on
>> a language pragma.
>>
>> How do people feel about a cosmetic fix, where we introduce a new
>> pragma, {-# LANGUAGE ShowLevity #-} which controls the display of levity
>> arguments/TYPE.  It's off by default but gets turned on by some
>> extensions like MagicHash (i.e. we only show levity if you have
>> enabled extensions where the distinction matters).
>>
>> Edward
>>
>> Excerpts from Christopher Allen's message of 2016-02-04 15:20:34 -0800:
>> > This seems worse than FTP IMO. It's considerably noisier, considerably
>> > rarer a concern for Haskell programmers, and is wa beyond the scope
>> of
>> > most learning resources.
>> >
>> > Is there a reason this isn't behind a pragma?
>> >
>> > On Thu, Feb 4, 2016 at 5:02 PM, Manuel M T Chakravarty <
>> c...@justtesting.org
>> > > wrote:
>> >
>> > > To be honest, I think, it is quite problematic if an obscure and
>> untested
>> > > language extension (sorry, but that’s what it is right now) bleeds
>> through
>> > > into supposedly simple standard functionality. The beauty of most of
>> GHC’s
>> > > language extensions is that you can ignore them until you need them.
>> > >
>> > > Has this ever been discussed more widely? I expect that every single
>> > > person teaching Haskell is going to be unhappy about it.
>> > >
>> > > Manuel
>> > >
>> > >
>> > > > Richard Eisenberg :
>> > > >
>> > > > I agree with everything that's been said in this thread, including
>> the
>> > > unstated "that type for ($) is sure ugly".
>> > > >
>> > > > Currently, saturated (a -> b) is like a language construct, and it
>> has
>> > > its own typing rule, independent of the type of the type constructor
>> (->).
>> > > But reading the comment that Ben linked to, I think that comment is
>> out of
>> > > date. Now that we have levity polymorphism, we can probably to the
>> Right
>> > > Thing and make the kind of (->) more flexible.
>> > > >
>> > > > Richard
>> > > >
>> > > > On Feb 4, 2016, at 3:27 PM, Ryan Scott 
>> wrote:
>> > > >
>> > > >>> My understanding was that the implicitly polymorphic levity, did
>> (->)
>> > > not change because it's a type constructor?
>> > > >>
>> > > >> The kind of (->) as GHCi reports it is technically correct. As a
>> kind
>> > > >> constructor, (->) has precisely the kind * -> * -> *. What's
>> special
>> > > >> about (->) is that when you have a saturated application of it, it
>> > > >> takes on a levity-polymorphic kind. For example, this:
>> > > >>
>> > > >>   :k (->) Int# Int#
>> > > >>
>> > > >> would yield a kind error, but
>> > > >>
>> > > >>   :k Int# -> Int#
>> > > >>
>> > > >> is okay. Now, if you want an explanation as to WHY that's the
>> case, I
>> > > >> don't think I could give one, as I simply got this information from
>> > > >> [1] (see the fourth bullet point, for OpenKind). Perhaps SPJ or
>> > > >> Richard Eisenberg could give a little insight here.
>> > > >>
>> > > >>> Also does this encapsulate the implicit impredicativity of ($) for
>> > > making runST $ work? I don't presently see how it would.
>> > > >>
>> > > >> You're right, the impredicativity hack is a completely different
>> > > >> thing. So while you won't be able to define your own ($) and be
>> able
>> > > >> to (runST $ do ...), you can at least define your own ($) and have
>> it
>> > > >> work with unlifted return types. :)
>> > > >>
>> > > >> Ryan S.
>> > > >> -
>> > > >> [1] https://ghc.haskell.org/trac/ghc/wiki/NoSubKinds
>> > > >>
>> > > >> On Thu, Feb 4, 2016 at 2:53 PM, Christopher Allen <
>> c...@bitemyapp.com>
>> > > wrote:
>> > > >>> My understanding was that the implicitly polymorphic levity, did
>> (->)
>> > > not
>> > > >>> change because it's a type constructor?
>> > > >>>
>> > > >>> Prelude> :info (->)
>> > > >>> data (->) a b -- Defined in ‘GHC.Prim’
>> > > >>> Prelude> :k (->)
>> > > >>> (->) :: * -> * -> *
>> > > >>>
>> > > >>> Basically I'm asking why ($) changed and (->) did not when (->)
>> had
>> > > similar
>> > > >>> properties WRT * and #.
>> > > >>>
>> > > >>> Also does this encapsulate the implicit impredicativity of ($) for
>> > > making
>

Re: equality relations: user-facing pretty-printing question

2016-01-18 Thread Iavor Diatchki
Hello,

What's the difference between `~~` and `~#` (I assume `~#` is
heterogeneous)?

As for the rest, as far as I understand, `~` is a strict subset of `~~` in
the sense that:
  1. if `a ~ b`, then `a ~~ b`
  2. if `not (a ~ b)`, then `not (a ~~ b)`
  3. if `a ~ b` is a kind error (i.e., the kind of `a` is known to be
different from the kind of `b`), then `not (a ~~ b)`

So, perhaps it makes sense to have a "smart" pretty printer for `a ~ b`:

  if kindOf a == kindOf b then `a ~ b` else `a ~~ b`

-Iavor







On Mon, Jan 18, 2016 at 9:24 AM, Ryan Scott  wrote:

> In my ideal world, GHC would remember as much as what the user wrote
> as possible in printing error messages. So if the user writes:
>
> f :: Int ~ Char => ...
>
> Then GHC would remember that the context was written with a single
> tilde, and print out Int ~ Char in the error message explicitly
> wherever the full type signature of f is printed.
>
> What it sounds like, though, is that deep in the guts of the type
> inferencer, there's a chance that single-tilde equality might turn
> into double-tilde or tilde-hash equality at some point. In those
> cases, printing out the particular brand of tilde might get confusing.
> In such cases, we might compromise and print out something neutral
> like "is equal to". I suppose this would always be the case if you
> didn't explicitly write a ~ b and had to infer it.
>
> I'm not sure about the technical details of this though, i.e., if GHC
> actually remembers a ~ b all the way through the
> typechecking/inferencing pipeline.
>
> Ryan S.
> ___
> 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: Further custom type error questions

2015-11-16 Thread Iavor Diatchki
Hello,

I imagine people wanting to do things as in the example below.  If we were
to use only `TypeError` constraints, then we'd have to mostly use the class
system to do type-level evaluation.  It doesn't seem obvious how to do that
with just `TypeError` of kind constraint, unless all evaluation was to
happen using the class system.

-Iavor
PS: Interestingly, this example reveals a bug with GHC's new warning about
unused constraints, where the `OffsetOf` constant on `get` is reported as
unnecessary...  I'll file a bug.


{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances, DataKinds
#-}
{-# LANGUAGE ScopedTypeVariables #-}

import GHC.TypeLits
import Data.Proxy
import Data.Word
import Foreign.Ptr

type OffsetOf l xs = GetOffset 0 l xs

type family ByteSize x where
  ByteSize Word64   = 8
  ByteSize Word32   = 4
  ByteSize Word16   = 2
  ByteSize Word8= 1
  ByteSize a= TypeError (Text "The type " :<>: ShowType a :<>:
 Text " is not exportable.")

type family GetOffset n (l :: Symbol) xs where
  GetOffset n l ( '(l,a) ': xs) = '(n,a)
  GetOffset n l ( '(x,a)  : xs) = GetOffset (n+ByteSize a) l xs
  GetOffset n l '[] = TypeError (Text "Missing field: " :<>:

ShowType l)

newtype Struct (a :: [(Symbol,*)]) = Struct (Ptr ())


get :: forall l fs n a.
  (OffsetOf l fs ~ '(n,a), KnownNat n) =>
  Struct fs ->
  Proxy l   ->
  Ptr a
get (Struct p) _ = plusPtr p (fromInteger (natVal (Proxy :: Proxy n)))


type MyStruct = [ '("A",Word8), '("B",Word8), '("C",Int) ]

testOk :: Struct MyStruct -> Ptr Word8
testOk s = get s (Proxy :: Proxy "B")


{-
testNotOk :: Struct MyStruct -> Ptr Word8
testNotOk s = get s (Proxy :: Proxy "X")
--}

{-
type MyOtherStruct = [ '("A",Int), '("B",Word8) ]

testNotOk :: Struct MyOtherStruct -> Ptr Word8
testNotOk s = get s (Proxy :: Proxy "B")
--}







On Mon, Nov 16, 2015 at 1:21 PM, Ben Gamari  wrote:

>
> While preparing some additional documentation for Iavor's custom type
> errors work (which has been merged; thanks Iavor!) I noticed that
> Dominique Devriese has raised some additional questions on the proposal
> [1].
>
> In particular, Dominique suggests that perhaps TypeError should simply
> be of kind `ErrorMessage -> Constraint`. My understanding of the
> proposal is that the intention is that `TypeError`s should be usable on
> the RHS of type functions, like `error` on the term level. However, is
> this strictly necessary? Is there any place where you couldn't just as
> easily express the `TypeError` as a constraint?
>
> If not, it seems like this may be substantially simpler approach and
> totally side-steps the detection of `TypeError` in inappropriate places
> on the RHS.
>
> Regardless, it seems like this (and the other questions) is worth
> addressing in the proposal.
>
> Cheers,
>
> - Ben
>
>
> [1]
> https://ghc.haskell.org/trac/ghc/wiki/Proposal/CustomTypeErrors#SomedesignquestionsDominiqueDevriese
> :
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Type-level error messages

2015-10-29 Thread Iavor Diatchki
Hello,

I've updated the implementation to match the discussion from this morning.
The idea is that `TypeError msd` is a type-family that can never be
reduced, similar to `Any`.  We don't do anything special in the constraint
solver, however when printing errors, if we encounter any constraints of
the form:
  * TypeError msg
  * TypeError msg ~ Something
  * Something ~ TypeError msg

Then we evaluate `msg` and use it as the error message.

This is fairly simple, and appears to work quite well.  The implementation
is on branch `wip/custom-type-errors`  (
https://github.com/ghc/ghc/tree/wip/custom-type-errors).


== Arc Difficulties Below ===

I tried to update the Phabricator patch but failed.  This is what I did:

1. arc diff master --update D1236 --head custom-type-errors

Exception
ERR-CONDUIT-CALL: API Method "differential.creatediff" does not define
these parameters: 'arcanistProject'.
(Run with `--trace` for a full exception trace.)

2. I thought that maybe I need to update `arcanist`, so I pulled the latest
version for git.

3. arc diff master --update D1236 --head custom-type-errors

Exception
Failed to load class or interface 'PhutilClassMapQuery': the class or
interface 'PhutilClassMapQuery' is not defined in the library map for any
loaded phutil library. If this symbol was recently added or moved, your
library map may be out of date. You can rebuild the map by running 'arc
liberate'. For more information, see:
http://www.phabricator.com/docs/phabricator/article/libphutil_Libraries_User_Guide.html
(Run with `--trace` for a full exception trace.)

4. arc liberate

Exception
Failed to load class or interface 'PhutilClassMapQuery': the class or
interface 'PhutilClassMapQuery' is not defined in the library map for any
loaded phutil library. If this symbol was recently added or moved, your
library map may be out of date. You can rebuild the map by running 'arc
liberate'. For more information, see:
http://www.phabricator.com/docs/phabricator/article/libphutil_Libraries_User_Guide.html
(Run with `--trace` for a full exception trace.)


Any advice on what I am doing wrong?

-Iavor




















On Wed, Oct 28, 2015 at 10:17 AM, Iavor Diatchki 
wrote:

> I have also written my thoughts on the questions posed by Richard on the
> wiki page.
>
>
>
>
> On Wed, Oct 28, 2015 at 7:07 AM, Richard Eisenberg 
> wrote:
>
>>
>> On Oct 28, 2015, at 10:02 AM, "Augustsson, Lennart" <
>> lennart.augusts...@sc.com> wrote:
>>
>> > I've put in my answers to your questions.
>>
>> And I've responded.
>
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Type-level error messages

2015-10-28 Thread Iavor Diatchki
I have also written my thoughts on the questions posed by Richard on the
wiki page.




On Wed, Oct 28, 2015 at 7:07 AM, Richard Eisenberg 
wrote:

>
> On Oct 28, 2015, at 10:02 AM, "Augustsson, Lennart" <
> lennart.augusts...@sc.com> wrote:
>
> > I've put in my answers to your questions.
>
> And I've responded.
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Type-level error messages

2015-10-27 Thread Iavor Diatchki
Hi Ben,

I updated the wiki page for GHC 8.0.1 to add an entry for the custom type
errors (under "in flight, but likely to make it").  It shouldn't be a
problem to make all changes needed by the end of November.

Ther phabricator link is this:
https://phabricator.haskell.org/D1236

The ticket is here:
https://ghc.haskell.org/trac/ghc/ticket/9637


Disclaimer: I don't really understand the phabricator work-flow, I just
 blindly followed the instructions on the wiki to create this, but I don't
really know how to update it or make changes to it.  I'd be happy to push a
standard git branch, if that would be useful for you.  It certainly would
be easier for me, as I have a good mental model of what git does, but have
only very rudimentary understanding of phabricator.

-Iavor





On Tue, Oct 27, 2015 at 11:27 AM, Ben Gamari  wrote:

> Iavor Diatchki  writes:
>
> > Hello,
> >
> Hello!
>
> Very good timing on the message; we just finished discussing your work
> not more than an hour ago. You can disregard my message; I didn't notice
> yours before sending it.
>
> > On Thu, Oct 22, 2015 at 9:47 AM, Simon Peyton Jones <
> simo...@microsoft.com>
> > wrote:
> >
> >> I’ve forgotten the state of your type-level error messages work.  How’s
> it
> >> going?
> >>
> >> I think we should try to add it to 8.0.1.  The current status is that
> the
> >> idea is implemented on a branch.  Then, there were some comments and
> >> suggestions that maybe we should do things in a different way,
> >> implementation wise.  I haven't had a chance to look into these in
> detail,
> >> or implement them, and as far as I know nobody else has stepped up to
> make
> >> the changes.  So we could simply go with the current version, and if for
> >> some reason we want to change the implementation we could do it later,
> as I
> >> don't think the API will be affected in any way.When do the changes
> >> need to happen by, so that it makes it in 8.0?   I have been a bit busy,
> >> but I could probably find some time to make whatever changes are
> required
> >> for this to be merged.
> >>
> >> OK good!  In that case
> >>
> >> · Add it to the hoped-for features in the GHC 8.01. status page
> >>
> > Where is the GHC 8.01 status page?
> >
> Here,
>
> https://ghc.haskell.org/trac/ghc/wiki/Status/GHC-8.0.1
>
> > · Write a wiki page with a specification
> >>
> >> Here is the specification:
> > https://ghc.haskell.org/trac/ghc/wiki/CustomTypeErros
> >
> Great! I have moved this to,
>
> https://ghc.haskell.org/trac/ghc/wiki/Proposal/CustomTypeErrors
>
> and left a redirect page in the old location.
>
> Is there a Trac ticket for this?
>
> >
> >> · Announce the proposal and seek feedback
> >>
> > We already had a discussion about it, there are notes on the wiki.  I
> don't
> > think any of the comments were about the actual design, the comments seem
> > to be more about the implementation.  On that front, if I am to make the
> > necessary changes, maybe we could have a chat (or e-mail conversation) to
> > make sure that I understand the changes and the motivation for them---the
> > wiki is not a great media for question/answer type of discussions.
> >
> I'll let you and Simon work this out.
>
> >> · Meanwhile make sure the branch reflects what you want to be in
> >> it
> >>
> >> I think that the branch should be in an OK state, except that it is not
> > merged with the latest HEAD.
> >
> Where can this branch be found?
>
> Cheers,
>
> - Ben
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Type-level error messages

2015-10-27 Thread Iavor Diatchki
Hello,

On Thu, Oct 22, 2015 at 9:47 AM, Simon Peyton Jones 
wrote:

> I’ve forgotten the state of your type-level error messages work.  How’s it
> going?
>
> I think we should try to add it to 8.0.1.  The current status is that the
> idea is implemented on a branch.  Then, there were some comments and
> suggestions that maybe we should do things in a different way,
> implementation wise.  I haven't had a chance to look into these in detail,
> or implement them, and as far as I know nobody else has stepped up to make
> the changes.  So we could simply go with the current version, and if for
> some reason we want to change the implementation we could do it later, as I
> don't think the API will be affected in any way.When do the changes
> need to happen by, so that it makes it in 8.0?   I have been a bit busy,
> but I could probably find some time to make whatever changes are required
> for this to be merged.
>
>
>



> OK good!  In that case
>
> · Add it to the hoped-for features in the GHC 8.01. status page
>
Where is the GHC 8.01 status page?

· Write a wiki page with a specification
>
> Here is the specification:
https://ghc.haskell.org/trac/ghc/wiki/CustomTypeErros


> · Announce the proposal and seek feedback
>
We already had a discussion about it, there are notes on the wiki.  I don't
think any of the comments were about the actual design, the comments seem
to be more about the implementation.  On that front, if I am to make the
necessary changes, maybe we could have a chat (or e-mail conversation) to
make sure that I understand the changes and the motivation for them---the
wiki is not a great media for question/answer type of discussions.


> · Meanwhile make sure the branch reflects what you want to be in
> it
>
> I think that the branch should be in an OK state, except that it is not
merged with the latest HEAD.


-Iavor







>
> If you don’t have time, well, no harm done… any progress you make on the
> above will still be useful.
>
>
>
> Simon
>
>
>
> *From:* Iavor Diatchki [mailto:iavor.diatc...@gmail.com]
> *Sent:* 22 October 2015 17:42
> *To:* Simon Peyton Jones
> *Cc:* Augustsson, Lennart
> *Subject:* Re: Type-level error messages
>
>
>
> Hello,
>
>
>
> I think we should try to add it to 8.0.1.  The current status is that the
> idea is implemented on a branch.  Then, there were some comments and
> suggestions that maybe we should do things in a different way,
> implementation wise.  I haven't had a chance to look into these in detail,
> or implement them, and as far as I know nobody else has stepped up to make
> the changes.  So we could simply go with the current version, and if for
> some reason we want to change the implementation we could do it later, as I
> don't think the API will be affected in any way.When do the changes
> need to happen by, so that it makes it in 8.0?   I have been a bit busy,
> but I could probably find some time to make whatever changes are required
> for this to be merged.
>
>
>
> -Iavor
>
>
>
>
>
>
>
>
>
>
>
>
>
> On Thu, Oct 22, 2015 at 3:47 AM, Simon Peyton Jones 
> wrote:
>
> Iavor
>
> I’ve forgotten the state of your type-level error messages work.  How’s it
> going?
>
> It’s not mentioned on
> https://ghc.haskell.org/trac/ghc/wiki/Status/GHC-8.0.1: shouldn’t it be?
>
> Simon
>
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: [RFC] Moving user's guide to ReStructuredText

2015-09-23 Thread Iavor Diatchki
Hello,

thanks for doing this Ben!  +1 for me too.  Like others, I don't like
editing XML by hand.   As to which other format to use, I trust your
judgement---I've used a bunch of them, and in my mind they are all fairly
similar, and I always have to look up how exactly things work anyway, so
whatever seems reasonable.

-Iavor



On Wed, Sep 23, 2015 at 5:09 AM, Ben Gamari  wrote:

> Ben Gamari  writes:
>
> > Hello all!
> >
> I have collected the details of this proposal into a Wiki page[1]. Feel
> free to leave thoughts there as well as this thread.
>
> Cheers,
>
> - Ben
>
>
> [1] https://ghc.haskell.org/trac/ghc/wiki/UsersGuide/MoveFromDocBook
>
> ___
> 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: OVERLAPPABLE/OVERLAPPING/OVERLAPS pragmas are confusing

2015-08-25 Thread Iavor Diatchki
Johan,

to summarize:

1. If an instance is marked as OVERLAPPABLE, then clients may overlap it
without having any pragmas
2. If an instance is NOT marked OVERLAPPABLE, then clients may still
overlap it, but then they have to use an explicit OVERLAPPING pragma.

So you should either add OVERLAPPABLE to your library, and then clients
don't need to do anything, or
you should remove it, and require that clients add OVERLAPPING.

Note that using this mechanism across modules can be quite error prone.
For example, you have to be very careful
not to use an OVERLAPPABLE instance in your library, as if you do parts of
the program might end up using
one instance, and other parts may end up using another instance---GHC has
no way of knowing about overlapping
instance in client libraries, so it will simply use the best possible
*local* instance.

-Iavor













On Tue, Aug 25, 2015 at 8:46 AM, Mikhail Glushenkov <
the.dead.shall.r...@gmail.com> wrote:

> Hi,
>
> On 25 August 2015 at 14:18, Johan Tibell  wrote:
> > The proposed change to my library is here:
> > https://github.com/tibbe/cassava/pull/95/files
> >
> > We remove the OverlappingInstances pragma and instead add an OVERLAPPABLE
> > pragma like so:
> >
> > instance {-# OVERLAPPABLE #-} FromField a => FromField (Maybe a)
> where
> >
> > This causes clients of the library that previously compiled (e.g. the
> > music-parts package) to no longer compile, due to a now lacking
> OVERLAPPING
> > pragma in their code.
>
> No, it's not quite like that. Client code can start to break when {-#
> LANGUAGE OverlappingInstances #-} is removed, as happened with the
> music-parts package. Adding an OVERLAPPABLE pragma to cassava's code
> made that error go away.
>
> Client code can usually work around the problem of missing
> OVERLAPPABLE pragmas in the library by adding OVERLAPPING pragmas to
> their instances. The reason I suggested bumping cassava's version is
> that there may be some places in cassava that still need new pragmas
> that I've overlooked.
>
> If GHC had an option for detecting overlapping instances at definition
> site, that'd help, I think, since then it'd be easier to find
> instances that need new pragmas.
> ___
> 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: Typechecker / OverloadedStrings question 7.8 vs. 7.10

2015-08-03 Thread Iavor Diatchki
Hello,

what Reid says is exactly right---the issue is not really about what
instances are present, the problem is that GHC can't determine how to
instantiate `t0`.
Perhaps a more direct way to describe this is as follows:

Failed to infer type `t0`
  while solving constraint `Data.String.IsString (t0 Char)`
  arising from the use of:
elem :: a -> t0 a -> Bool

-Iavor





On Mon, Aug 3, 2015 at 9:47 AM, Brandon Allbery  wrote:

> On Mon, Aug 3, 2015 at 12:45 PM, Daniel Bergey 
> wrote:
>
>> I thought GHC would infer the type when only one instance is in scope,
>> at least in some cases, like IsString.  But I could well be wrong about
>> that.
>>
>
> Typeclasses are open-world; this is not a safe assumption, since instances
> are global and an instance added elsewhere at some point in the future
> could therefore break your program.
>
> --
> brandon s allbery kf8nh   sine nomine
> associates
> allber...@gmail.com
> ballb...@sinenomine.net
> unix, openafs, kerberos, infrastructure, xmonad
> http://sinenomine.net
>
> ___
> 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: Fundep question

2015-07-31 Thread Iavor Diatchki
Yeah, this should work with UndecidableInstances.  The reason you need that
extension is that if we consider the context, then there are some
pathological examples that can make GHC's instance checking algorithm go
forever.

On Fri, Jul 31, 2015 at 9:56 AM, Gabor Greif  wrote:

> No. I'll switch that on and report back.
>
> Thanks,
>
> Gabor
>
>
> Em sexta-feira, 31 de julho de 2015, Simon Peyton Jones <
> simo...@microsoft.com> escreveu:
>
>> you need "liberal coverage checking", so UndecidableInstances. Are you
>> doing that?
>>
>> |  -Original Message-
>> |  From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of
>> |  Richard Eisenberg
>> |  Sent: 31 July 2015 16:10
>> |  To: Gabor Greif
>> |  Cc: ghc-devs
>> |  Subject: Re: Fundep question
>> |
>> |  Let's rewrite with explicit kind variables, noting that b is also
>> |  poly-kinded:
>> |
>> |  class Dep k k2 (a :: k) (b :: k2) | a -> b k2
>> |  -- if a determines b, it surely determines k2
>> |
>> |  instance Dep k * x y => Dep (Maybe k) * (Just x) (Maybe y)
>> |
>> |  Actually, even with the kinds explicit, it still looks valid to me.
>> |  Post a bug report?
>> |
>> |  Richard
>> |
>> |  On Jul 31, 2015, at 9:54 AM, Gabor Greif  wrote:
>> |
>> |  > Hi all,
>> |  >
>> |  > say I want to instantiate
>> |  >
>> |  >class Dep (a :: k) b | a -> b
>> |  >
>> |  > as
>> |  >
>> |  >instance Dep x y => Dep (Just x) (Maybe y)
>> |  >
>> |  > Is this supposed to work? I get "The coverage condition fails"
>> |  errors.
>> |  >
>> |  > For simple cases like
>> |  >
>> |  >instance Dep True Bool
>> |  >
>> |  > etc. it seems to work fine.
>> |  >
>> |  > Thanks and cheers,
>> |  >
>> |  >Gabor
>> |  > ___
>> |  > 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
>>
>
> ___
> 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: Interactions between type-checker plugins

2015-05-20 Thread Iavor Diatchki
newSimpleWanted (
> https://downloads.haskell.org/~ghc/7.10.1/docs/html/libraries/ghc-7.10.1/TcMType.html#v:newSimpleWanted)
> to create the new wanted constraint.
> But for some reason the errror message doesn't get the source-error
> location of the original constraint.
> Perhaps I shouldn't be using 'newSimpleWanted' to create new wanted
> constraints?
>
> The sources for the plugins are over here:
> https://github.com/christiaanb/ghc-typelits-natnormalise
> https://github.com/christiaanb/ghc-typelits-extra
>
> Cheers,
>
> Christiaan
>
>
>
> On 19 May 2015 at 18:01, Iavor Diatchki  wrote:
>
>> Hi Christiaan,
>>
>>
>> Plugins should return the solved constraints in the first field of
>> `TcPLuginOk`, and additional sub-goals in the second.
>> The constraints in the first list are marked as solved, and do not need
>> to be processed further,  while the constraints
>> in the second list will be added to the work queue, for further
>> processing.  Also, the solutions of wanted goals may be in terms of other
>> as yet unsolved things.
>>
>> I think that there are two situations when a plugin might return an empty
>> first list, but new work in the second list.
>> Both are about computing new facts, and thus "communicating" with other
>> plugins:
>>1. Discover new given facts:  the plugin was presented with some
>> givens, and it computed some additional givens that it thinks might be of
>> use to someone else (typically these are equality constraints)
>>2. Discover new derived facts:  the plugin was presented with a
>> mixture of wanted and givens, and it thinks that the new derived facts
>> might be useful by specializing the problemderived facts help with type
>> inference by instantiating unification variables.
>>
>> Generally, I don't think a plugin should ever need to emit new wanted
>> constraints without solving anything. It'd be interesting if that could
>> happen though...
>>
>> Another thing that might be relevant: at present, GHC's constraint solver
>> does not do back tracking.  So there is no way for a plugin (or other parts
>> of the constraint solver) to say: "I'll emit this new wanted constraint,
>> and depending on if it was proved or disproved do something".   Another way
>> to think of his is that constraints are either solved or unsolved, but
>> being unsolved does not mean that they are disproved.  Now, there is a
>> mechanism to mark a constraint as "never solvable", but currently this is
>> mostly used for error reporting.
>>
>> For your concrete example though, the plugin can actually commit to the
>> given path because the only way to solve "GCD 6 8 + x ~ x + GCD 9 6" is if
>> "GCD 6 8 ~ GCD 9 6".  So I'd imagine you want these steps:
>>
>> Plugin A: Solve "GCD 6 8 + x ~ x + GCD 9 6", new wanted "GCD 6 8 ~ GCD 9
>> 6"
>> Plugin B: "GCD 6 8 ~ GCD 9 6" --> impossible
>> Done.
>>
>>
>> -Iavor
>>
>>
>>
>> On Tue, May 19, 2015 at 3:35 AM, Christiaan Baaij <
>> christiaan.ba...@gmail.com> wrote:
>>
>>> I have a question about how type-checker plugins should interact.
>>> My situation is the following:
>>> I have two type-checker plugins, one that can solve equalities involving
>>> the standard type-level operations on kind Nat (+,*,-,^), and another
>>> type-checker plugin that can prove equalities involving a new type-level
>>> operation GCD.
>>> In the following, the type-checker plugin involving the stand type-level
>>> operations is called ‘A’, and the type checker involving the new GCD
>>> operations is called ‘B’.
>>>
>>> When type-checker plugin A encounters:
>>> [W] GCD 6 8 + x ~ x + GCD 9 6
>>>
>>> It knows that (+) is commutative, so it can prove the above equality
>>> _given_ that "GCD 6 8 ~ GCD 9 6” holds.
>>> So what type-checker plugin A does now is emits a new wanted constraints:
>>> [W] GCD 6 8 ~ GCD 9 6
>>> And remembers that it emitted this wanted constraint.
>>> In type-checker plugin lingo, it returns:
>>> TcPluginOk [] ["[W] GCD 6 8 ~ GCD 9 6”]
>>>
>>>
>>
>> Now whenever type-checker plugin encounters
>>> [W] GCD 6 8 + x ~ x + GCD 9 6
>>> again, it checks to see if the discharged constraint
>>> [W] GCD 6 8 ~ GCD 9 6
>>> Is already solved, is disproven, or unsolved.
>>> If the discharged co

Re: deriving Typeable and Nat kinds

2015-04-23 Thread Iavor Diatchki
Could you please make a ticket for this, so that we have a reference and it
does not get lost?

On Thu, Apr 23, 2015 at 9:59 AM, Iavor Diatchki 
wrote:

> Aha, I see what happened.  What I said before was wrong---indeed the
> `Typeable` instance for type-nats (and symbols) used to be implemented in
> terms of `KnownNat` and `KnownSymbol`:
>
> instance KnownNat n => Typeable (n :: Nat) where ...
>
> When I updated the `Typeable` solver, I forgot about that special
> case---I'll have a go at a fix.
>
> -Iavor
>
>
>
>
> On Thu, Apr 23, 2015 at 8:37 AM, Gabor Greif  wrote:
>
>> On 4/23/15, Iavor Diatchki  wrote:
>> > Hello,
>> >
>>
>> Hi Iavor,
>>
>> > Apologies if my changes caused difficulties with your work---we made the
>> > changes to `Typable` to preserve the soundness of the type system,
>> > hopefully the new behavior is exactly equivalent to the old in the safe
>> > cases.
>>
>> No need to apologize, I chose this way to be able to intervene fast
>> when something breaks :-) The old behaviour might have been unsafe,
>> though I cannot see why.
>>
>> >
>> > Could you post an example of the code where the unwanted `Typeable p`
>> > constraint appears?  It seems entirely reasonable that if you want to
>> solve
>> > `Typeable (OUT p o)`, you'll have to provide `Typealbe p`, so I am not
>> > seeing the whole picture.
>>
>> Here is a small example where an additional constraint surfaces:
>>
>>
>> --
>> {-# LANGUAGE AutoDeriveTypeable, GADTs, DataKinds, KindSignatures,
>> StandaloneDeriving #-}
>>
>> import GHC.TypeLits
>> import Data.Typeable
>>
>> data Foo (n :: Nat) where
>>   Hey :: KnownNat n => Foo n
>>
>> deriving instance Show (Foo n)
>>
>> data T t where
>>   T :: (Show t, Typeable t) => t -> T t
>>
>> deriving instance Show (T n)
>>
>> {-
>>
>> ---  WITH ghci-7.11.20150407 (and newer)
>> *Main> :t T Hey
>> T Hey :: (Typeable n, KnownNat n) => T (Foo n)
>>
>> ---  WITH ghci-7.11.20150215 (old)
>> *Main> :t T Hey
>> T Hey :: KnownNat n => T (Foo n)
>>
>> -}
>>
>> --
>>
>>
>> >
>> > To answer your question about `KnownNat p`---there is no relation
>> between
>> > it and `Typeable`.   You may think if a `KnownNat x` constraint as just
>> the
>> > integer `x`.  As it happens, the integer is closely related to the
>> > `Typeable` instance for the number, so I think we *could* make it work
>> so
>>
>> Yes, this relation I was alluding to.
>>
>> > that if you have `KnownNat p`, then you can get `Typeable p`, but this
>> has
>> > never worked previosly, so perhaps there is another issue.
>>
>> Maybe with my example from above it might be easier to debug it.
>>
>> >
>> > -Iavor
>>
>> Thanks,
>>
>> Gabor
>>
>> >
>> >
>> >
>> > On Thu, Apr 23, 2015 at 7:04 AM, Gabor Greif  wrote:
>> >
>> >> Hi devs,
>> >>
>> >> between ghc-7.11.20150215 and ghc-7.11.20150407 I experienced a
>> >> strange regression with deriving Typeable for data with Nat-kinded
>> >> indices.
>> >>
>> >> Something like this used to work (I cannot post the whole thing,
>> >> unfortunately)
>> >>
>> >> {{{
>> >> data OTU (p :: Nat) (o :: Nat) = OTU { ...fields... } deriving (Show,
>> >> Typeable)
>> >> }}}
>> >>
>> >> With my ghc-7.11.20150407 (and later) strange obligations of the form
>> >> `Typeable p` appear, rendering my code uncompilable. But there is no
>> >> way I can see how I can convince the type checker that the Nat index
>> >> is indeed Typeable. I *do* have a `KnownNat p` constraint around,
>> >> though.
>> >>
>> >> The relevant changes to mainline appear to be
>> >>
>> https://github.com/ghc/ghc/commit/b359c886cd7578ed083bcedcea05d315ecaeeb54
>> >>
>> https://github.com/ghc/ghc/commit/3a0019e3672097761e7ce09c811018f774febfd2
>> >>
>> >> both by Iavor.
>> >>
>> >> So now my questions:
>> >>
>> >> 1) Is this a regression on mainline? (I surely hope so!) How did this
>> >> work before?
>> >> 2) Should `KnownNat p` imply `Typeable p` for the ability to have my
>> >> `Typeable (OTU p o)`
>> >> 3) if 2) is answered with "NO", how am I supposed to satisfy those
>> >> constraints?
>> >>
>> >> Thanks and cheers,
>> >>
>> >> Gabor
>> >>
>> >>
>> >> PS: Sometimes I feel like a canary doing my research-like programming
>> >> with GHC-HEAD, and it is a mostly positive experience, but events like
>> >> this make me shiver...
>> >>
>> >
>>
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: deriving Typeable and Nat kinds

2015-04-23 Thread Iavor Diatchki
Aha, I see what happened.  What I said before was wrong---indeed the
`Typeable` instance for type-nats (and symbols) used to be implemented in
terms of `KnownNat` and `KnownSymbol`:

instance KnownNat n => Typeable (n :: Nat) where ...

When I updated the `Typeable` solver, I forgot about that special
case---I'll have a go at a fix.

-Iavor




On Thu, Apr 23, 2015 at 8:37 AM, Gabor Greif  wrote:

> On 4/23/15, Iavor Diatchki  wrote:
> > Hello,
> >
>
> Hi Iavor,
>
> > Apologies if my changes caused difficulties with your work---we made the
> > changes to `Typable` to preserve the soundness of the type system,
> > hopefully the new behavior is exactly equivalent to the old in the safe
> > cases.
>
> No need to apologize, I chose this way to be able to intervene fast
> when something breaks :-) The old behaviour might have been unsafe,
> though I cannot see why.
>
> >
> > Could you post an example of the code where the unwanted `Typeable p`
> > constraint appears?  It seems entirely reasonable that if you want to
> solve
> > `Typeable (OUT p o)`, you'll have to provide `Typealbe p`, so I am not
> > seeing the whole picture.
>
> Here is a small example where an additional constraint surfaces:
>
>
> --
> {-# LANGUAGE AutoDeriveTypeable, GADTs, DataKinds, KindSignatures,
> StandaloneDeriving #-}
>
> import GHC.TypeLits
> import Data.Typeable
>
> data Foo (n :: Nat) where
>   Hey :: KnownNat n => Foo n
>
> deriving instance Show (Foo n)
>
> data T t where
>   T :: (Show t, Typeable t) => t -> T t
>
> deriving instance Show (T n)
>
> {-
>
> ---  WITH ghci-7.11.20150407 (and newer)
> *Main> :t T Hey
> T Hey :: (Typeable n, KnownNat n) => T (Foo n)
>
> ---  WITH ghci-7.11.20150215 (old)
> *Main> :t T Hey
> T Hey :: KnownNat n => T (Foo n)
>
> -}
>
> --
>
>
> >
> > To answer your question about `KnownNat p`---there is no relation between
> > it and `Typeable`.   You may think if a `KnownNat x` constraint as just
> the
> > integer `x`.  As it happens, the integer is closely related to the
> > `Typeable` instance for the number, so I think we *could* make it work so
>
> Yes, this relation I was alluding to.
>
> > that if you have `KnownNat p`, then you can get `Typeable p`, but this
> has
> > never worked previosly, so perhaps there is another issue.
>
> Maybe with my example from above it might be easier to debug it.
>
> >
> > -Iavor
>
> Thanks,
>
> Gabor
>
> >
> >
> >
> > On Thu, Apr 23, 2015 at 7:04 AM, Gabor Greif  wrote:
> >
> >> Hi devs,
> >>
> >> between ghc-7.11.20150215 and ghc-7.11.20150407 I experienced a
> >> strange regression with deriving Typeable for data with Nat-kinded
> >> indices.
> >>
> >> Something like this used to work (I cannot post the whole thing,
> >> unfortunately)
> >>
> >> {{{
> >> data OTU (p :: Nat) (o :: Nat) = OTU { ...fields... } deriving (Show,
> >> Typeable)
> >> }}}
> >>
> >> With my ghc-7.11.20150407 (and later) strange obligations of the form
> >> `Typeable p` appear, rendering my code uncompilable. But there is no
> >> way I can see how I can convince the type checker that the Nat index
> >> is indeed Typeable. I *do* have a `KnownNat p` constraint around,
> >> though.
> >>
> >> The relevant changes to mainline appear to be
> >>
> https://github.com/ghc/ghc/commit/b359c886cd7578ed083bcedcea05d315ecaeeb54
> >>
> https://github.com/ghc/ghc/commit/3a0019e3672097761e7ce09c811018f774febfd2
> >>
> >> both by Iavor.
> >>
> >> So now my questions:
> >>
> >> 1) Is this a regression on mainline? (I surely hope so!) How did this
> >> work before?
> >> 2) Should `KnownNat p` imply `Typeable p` for the ability to have my
> >> `Typeable (OTU p o)`
> >> 3) if 2) is answered with "NO", how am I supposed to satisfy those
> >> constraints?
> >>
> >> Thanks and cheers,
> >>
> >> Gabor
> >>
> >>
> >> PS: Sometimes I feel like a canary doing my research-like programming
> >> with GHC-HEAD, and it is a mostly positive experience, but events like
> >> this make me shiver...
> >>
> >
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: deriving Typeable and Nat kinds

2015-04-23 Thread Iavor Diatchki
Hello,

Apologies if my changes caused difficulties with your work---we made the
changes to `Typable` to preserve the soundness of the type system,
hopefully the new behavior is exactly equivalent to the old in the safe
cases.

Could you post an example of the code where the unwanted `Typeable p`
constraint appears?  It seems entirely reasonable that if you want to solve
`Typeable (OUT p o)`, you'll have to provide `Typealbe p`, so I am not
seeing the whole picture.

To answer your question about `KnownNat p`---there is no relation between
it and `Typeable`.   You may think if a `KnownNat x` constraint as just the
integer `x`.  As it happens, the integer is closely related to the
`Typeable` instance for the number, so I think we *could* make it work so
that if you have `KnownNat p`, then you can get `Typeable p`, but this has
never worked previosly, so perhaps there is another issue.

-Iavor



On Thu, Apr 23, 2015 at 7:04 AM, Gabor Greif  wrote:

> Hi devs,
>
> between ghc-7.11.20150215 and ghc-7.11.20150407 I experienced a
> strange regression with deriving Typeable for data with Nat-kinded
> indices.
>
> Something like this used to work (I cannot post the whole thing,
> unfortunately)
>
> {{{
> data OTU (p :: Nat) (o :: Nat) = OTU { ...fields... } deriving (Show,
> Typeable)
> }}}
>
> With my ghc-7.11.20150407 (and later) strange obligations of the form
> `Typeable p` appear, rendering my code uncompilable. But there is no
> way I can see how I can convince the type checker that the Nat index
> is indeed Typeable. I *do* have a `KnownNat p` constraint around,
> though.
>
> The relevant changes to mainline appear to be
> https://github.com/ghc/ghc/commit/b359c886cd7578ed083bcedcea05d315ecaeeb54
> https://github.com/ghc/ghc/commit/3a0019e3672097761e7ce09c811018f774febfd2
>
> both by Iavor.
>
> So now my questions:
>
> 1) Is this a regression on mainline? (I surely hope so!) How did this
> work before?
> 2) Should `KnownNat p` imply `Typeable p` for the ability to have my
> `Typeable (OTU p o)`
> 3) if 2) is answered with "NO", how am I supposed to satisfy those
> constraints?
>
> Thanks and cheers,
>
> Gabor
>
>
> PS: Sometimes I feel like a canary doing my research-like programming
> with GHC-HEAD, and it is a mostly positive experience, but events like
> this make me shiver...
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Shake fails test with GHC 7.10 RC3

2015-03-21 Thread Iavor Diatchki
This is very odd---the example on the ticket does not use `Typeable` at all.

I looked through the diffs of the patch and I can't see anything obviously
wrong.

Also, the `Typeable` code only touches modules that are in the front-end,
and when I compile without optimizations, the example looks reasonable.

I wonder if the problem is related to some odd interaction between
simplification rules and representational equities?





On Sat, Mar 21, 2015 at 4:35 AM, Herbert Valerio Riedel 
wrote:

> On 2015-03-21 at 08:21:20 +0100, Herbert Valerio Riedel wrote:
> > On 2015-03-21 at 07:56:32 +0100, Neil Mitchell wrote:
> >
> > [...]
> >
> >> 3) I tested with GHC RC1 and GHC RC2, both of which were fine. The fact
> no
> >> one else hit this with RC2 might just be because its a very recent
> >> regression.
> >
> > We -- and by that I don't mean myself... :) -- could git-bisect between
> > RC2 and RC3 here (semi-)automatically (i.e. maybe unattended if it's
> > scriptable) if your test-case (even if it's not minimal) reliably
> > triggers the bug...
>
> I scripted up a test and git-bisected between RC2 and RC3, and the
> following commit is the one where `shake-test oracle test` starts
> failing
>
>
> http://git.haskell.org/ghc.git/commitdiff/6f46fe15af397d448438c6b93babcdd68dd78df8
>
> ...which sadly is a rather large patch :-/
> ___
> 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: Fwd: EvTerms and how they are used

2015-03-02 Thread Iavor Diatchki
Hello,

I've seen instances of this problem show up over and over again, and I
think that there is a more principled solution, based on the idea of
`improvement`.
The idea is to allow programmers to specify custom improvements.
Functional dependencies are one way to do this, but there is no reason why
this
should be the only way.   The details of this idea are explained in this
paper: "Simplifying and Improving Qualified Types" (
http://web.cecs.pdx.edu/~mpj/pubs/RR-1040.pdf).

In concrete Haskell syntax, this might work like this:

1. Add a new declaration:

  improve CS using EQs

Here the `CS` are a collection of constraints, and the `EQs` are a
collection of equations.

2. Modify the constraint solver, so that when it sees `CS` in the inert
set, it will emit the `EQs` as derived constraints.

This is all.

So now you can write things like this:

improve PolyMonad a b Identity using (a ~ Identity, b ~ Identity)

This tells GHC that it is OK to assume that if the final result is
`Identity`,
then the first two arguments will also be in the identity monad.

This is a fairly conservative extension, in that it is only used to
instantiate variables,
and it never needs to produce new equality proofs.  This is pretty much
exactly how FDs work
in the current implementation of GHC.  For example, the declaration:

class C a b | a -> b where ...

with GHC's current implementation, is exactly equivalent to:

class C a b where ...
improve (C a b, C a c) using (b ~ c)

Aside: GHC actually checks that all instances are consistent with the FD
declarations,
so GHC *could* use them to actually generate new evidence, but it does not
do so at the moment.

Anyway, implementing something like this should not be too hard, and it
seems that it could be
used not just for the PolyMonads work, but also for other cases where one
wants to write
specific improvements.

-Iavor

PS:  with GHC's current approach to resolving instances, you could also
avoid some of the
ambiguities for the `Identity` instance by writing it like this:

instance (a ~ Identity, b ~ Idnetity) => PolyMonad a b Identity where
...





























On Mon, Mar 2, 2015 at 8:38 AM, Jan Bracker 
wrote:

> Hi Adam,
>
> again thank you for your extensive and patient answer!
>
> It's a bit hard to know exactly what is going on without the full code,
>> but I think what is happening is this: you have an unsolved constraint
>> `Polymonad Identity n_abpq Identity` and your plugin provides an
>> evidence term of type `Polymonad Identity Identity Identity`, but of
>> course this is ill-typed, because `n_abpq` is not `Identity`. Hence Core
>> Lint quite reasonably complains.
>>
>
> I would have thought the constraint solver would derive that 'obviously'
> `n_abpq` needs to be unified with `Identity` and substitutes.
>
>
>> I'm not sure exactly what you are trying to do, but I think the right
>> way to approach this problem is to simulate a functional dependency on
>> Polymonad (in fact, can you use an actual functional dependency)?
>
>
> That is exactly what I _don't_ want to do. I am trying to achieve a more
> general version of monads, called polymonads as it was introduced here [1].
>
>
>> When confronted with the constraint `Polymonad Identity n_abpq Identity`,
>> do
>> not try to solve it directly, but instead notice that you must have
>> `n_abpq ~ Identity`. Your plugin can emit this as an additional derived
>> constraint, which will allow GHC's built-in solver to instantiate the
>> unification variable `n_abpq` and then solve the original constraint
>> using the existing instance. No manual evidence generation needed!
>>
>
> Yes, that makes perfect sense! I was so gridlocked, I did not see this as a
> possibility to solve the problem.
>
> Out of interest, can you say anything about your aims here? I'm keen to
>> find out about the range of applications of typechecker plugins.
>>
>
> I want to make Polymonads as proposed in [1] usable in Haskell. They
> generalize
> the bind operator to a more general signature `M a -> (a -> N b) -> P b`.
> Polymonads
> subsume the standard Monad as well as indexed or parameterized monad,
> without
> relying on functional dependencies, which can be limiting (there may be
> different
> requirement depending on the monad being implemented).
> Currently I am providing a type class for this:
>
> class Polymonad m n p where
>   (>>=) :: m a -> (a -> n b) -> p b
>
> As the paper points out in section 4.2 (Ambiguity), type inference breaks
> down,
> because the constraint solver is not able to solve the ambiguity. Here a
> small example:
>
> -- Return operator for the IO polymonad
> instance Polymonad Identity Identity IO where
>   -- ...
>
> -- Identity polymonad
> instance Polymonad Identity Identity Identity where
>   -- ...
>
> return :: (Polymonad Identity Identity m) => a -> m a
> return x = Identity x >>= Identity
>
> test :: Identity Bool
> test = do
>   x <- return True
>   return x
>
> For this exampl

Re: GHC Type Inference

2015-02-23 Thread Iavor Diatchki
Greetings,

The latest type-nat solver is available as a GHC plugin.  The repo is here:

https://github.com/yav/type-nat-solver

I just pushed a small fix-up and now it works with the GHC 7.10 release
candidate.  The plugin makes use of an external solver (the plugin is
currently hard-coded to use `cvc4` but we should really parametrize on
this).   I've not tested it a lot, but basic vector manipulation with GADTs
works fairly well, so you can do things like the examples at the end of the
e-mail.

If Marc---or anyone else---is interested in hacking on this, I'd be most
happy to collaborate, as I haven't had much time to work on this for the
last couple of a months.

We can push this is many interesting directions.  Here are some ideas:
   - Work on writing a Haskell based decision procedure;  this would remove
the need for calling an external tool
   - Explore and improve the current support for type naturals (e.g., add
rules to go beyond linear arithmetic).
   - Explore other theories:  the code in the current plugin happens to use
the theory of linear arithmetic, but most of the implementation is agnostic
to the actual theory used (apart from recognizing the symbols that belong
to the theory).  So we have an opportunity to explore potential uses of
other theories (e.g., bit-vectors at the type level could be used to
implement finite sets, or type-level modulo arithmetic;  some solvers have
experimental support for the theory of sets, so we could have interesting
reasoning about sets of various things: unions, intersections, etc).

Lots of interesting work to do, and not enough hacking time!

If there are questions, please drop me an e-mail directly, or we can chat
on the ghc-devs list, in case there are other interested developers.

Cheers,
-Iavor


Examples that work at the moment:


f :: ((a + 6) ~ x) => Proxy x -> ()
f = g

g :: ((6 <=? x) ~ True) => Proxy x -> ()
g _ = ()

data Vec :: Nat -> * -> * where
  Nil :: Vec 0 a
  Cons :: a -> Vec n a -> Vec (n + 1) a


append :: Vec m a -> Vec n a -> Vec (n + m) a
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

reverse = go Nil
  where
  go :: Vec m a -> Vec n a -> Vec (m + n) a
  go xs Nil = xs
  go xs (Cons y ys) = go (Cons y xs) ys


f1 :: Proxy (2 + a) -> ()
f1 = g1

g1 :: Proxy (1 + a) -> ()
g1 _ = ()










On Mon, Feb 23, 2015 at 2:53 PM, Simon Peyton Jones 
wrote:

> Marc
>
> For type-level literals, the man to talk to is Iavor Diatchki.  He
> implemented the current system, and has been working on enhancements.  I'm
> sure he'd welcome help!
>
> There's also quite an active sub-group (on ghc-devs) working on "plug-ins"
> for the type inference algorithm, aimed at allowing things like better
> arithmetic reasoning to be done without having to change GHC itself.
>
> Simon
>
> | -Original Message-
> | From: dongen [mailto:don...@cs.ucc.ie]
> | Sent: 23 February 2015 10:54
> | To: Simon Peyton Jones
> | Cc: ghc-devs@haskell.org
> | Subject: GHC Type Inference
> |
> | Dear Simon,
> |
> |
> | I am cc-ing _ghc-devs@haskell.org_ as requested on _ghc.haskell.org_.
> |
> | I hope you're fine.
> |
> | On _ghc.haskell.org_ I noticed you are the ``owner'' of _type
> | inference and interface files._
> |
> | A year ago I started a project that requires integer type-level
> | literals but I soon had to drop it because GHC wasn't able to
> | simplify simple type equalities. As a consequence, I had to
> | add lots and lots of constraints to make my code work, which
> | effectively meant the code became unmaintainable because a small
> | change requlted in lots of errors.
> |
> | I know have a bit more time to work on the project and I'd like
> | to see if it's possible to ``talk'' to somebody in the GHC team
> | to see if we can improve type-level literal inference for natural
> | numbers.
> |
> | Is there somebody who's ``responsible'' for this area in the GHC
> | team? If yes, would you mind giving me their contact details?
> |
> | Regards,
> |
> |
> | Marc van Dongen
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Phabricator question

2015-02-11 Thread Iavor Diatchki
Hello,

I followed the instruction on the GHC wiki, and published an `arc` revision
for my work on the typeable-with-kinds branch. The result was called D652.

After I did this, I noticed a bug, and some redundant code;  so I fixed my
branch.  How can I update D652, so that it will diff using the most current
version of my branch?

-Iavor
___
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs


  1   2   >