August 2012 - Glasgow-haskell-users

Question about type lits and optimization in ghc
by Iavor Diatchki 30 Aug '12

30 Aug '12

Hello, On Thu, Aug 23, 2012 at 2:03 AM, Simon Peyton-Jones <simonpj(a)microsoft.com>wrote: > I’m hazy about **** > > **· **the definitions of sing and fromSing > The family of singleton types, Sing, is quite general. However, when its parameter is of kind `Nat`, then it is simply a newtype for `Integer`: data family Sing (s :: a) newtype instance Sing (s :: Nat) = SingN Integer To access the `Integer` of a `Sing n` value we use the class `SingE`. Again, this is just so that we can support arbitrary singletons, but when the argument is of kind `Nat` we simply access the newtype's `Integer`: instance SingE (n :: Nat) Integer where fromSing (SingN x) = x Finally, `Sing n` values are introduced with the following class: class SingI n where sing :: Sing n The instances of this class when `n` is of kind `Nat` are built into GHC: when GHC needs to solve constraint like `SingI 5`, the solver provides a special piece of evidence, which is essentually 5 (actually, it is `EvLit (EvNum 5)`). When the evidence is desugered into Core, this is replaced with just the integer 5. (Aside: this is not strictly speaking correct---it should be replace with 5 coerced into `Sing 5`, which should then be coerced into the dictionary for `SingI 5`. These all have the same representation so things work for the time being, but this is certainly on my TODO list to correct). · **the transformations that are supposed to simplify (fromSing > (sing :: Sing c)) to c > So, now consider an expression like `fromSing (sing :: Sing 5)`. With explicit dictionaries it becomes: `fromSing d1 (sing d2)`. As we just discussed, `d2` is essentially 5, while `d1` will be the function in the `fromSing` instance above, which is really just a coercion because it accesses the field of a newtype. But note that so are `sing` and `fromSing` because they are methods of classes with just a single method! So this whole expressions really is a whole lot of coercions around 5, which is why I'd expect this kind of pattern to always be simplified. > **** > > **· **the details of the two examples you describe and what isn’t > happening that you expect to happen**** > > ** > Now for the example where I was expecting an optimization to happen but it did not. Consider the following program, with the two different definitions for `x`: main :: IO () main = print (fromInteger x :: Int) where x = 5 :: Integer -- x = fromSing (sing :: Sing 5) With the first definition, where `x` is simply 5, the interesting part of the Core looks like this: main2 :: String main2 = $wshowSignedInt 0 5 ([] @ Char) What's nice about this is that GHC has noticed that it does not need to make the intermediate `Integer` value, and replaced it with and `Int`. If we use the second definition for `x`, then we get a slightly less efficint version: main3 :: Type.Integer main3 = __integer 5 main2 :: String main2 = case integerToInt main3 of wild_ap2 { __DEFAULT -> $wshowSignedInt 0 wild_ap2 ([] @ Char) } Note that, for some reason, the call to `integerToInt` is not eliminated. I am not quite sure why that is. -Iavor > ** > > Can you give more specifics? > > S**** > > ** ** > > *From:* Iavor Diatchki [mailto:iavor.diatchki@gmail.com] > *Sent:* 23 August 2012 07:21 > *To:* Carter Schonwald > *Cc:* Simon Peyton-Jones > *Subject:* Re: question about type lits and optimization in ghc**** > > ** ** > > Hello,**** > > ** ** > > On Wed, Aug 22, 2012 at 10:15 PM, Carter Schonwald < > carter.schonwald(a)gmail.com> wrote:**** > > I'm asking about whether or no the compile time machinery of ghc will be > statically replacing "fromSing (sing :: Sing c)" with "c" when "c" is a > specific number at compile time. **** > > ** ** > > Yes, the intention is that this should be simplified into the > corresponding the value `c` of type `Integer`. I just run a small test. > This program:**** > > ** ** > > main :: IO ()**** > > main = print (fromSing (sing :: Sing 5))**** > > ** ** > > results in core which looks like this:**** > > ** ** > > main3 :: Integer**** > > main3 = __integer 5**** > > ** ** > > main2 :: [Char]**** > > main2 = $w$cshowsPrec 0 main3 []**** > > ** ** > > main1 :: State# RealWorld -> (# State# RealWorld, () #)**** > > main1 = \ eta_B1 -> hPutStr2 stdout main2 True eta_B1**** > > ** ** > > main4 :: State# RealWorld -> (# State# RealWorld, () #)**** > > main4 = \ eta_Xa -> runMainIO1 main1 eta_Xa**** > > ** ** > > This is pretty much the same code that one gets for `print 5`. I also > tried a variation:**** > > ** ** > > print (fromInteger (fromSing (sing :: Sing 5)) :: Int)**** > > ** ** > > While this also gets simplified to the integer 5, it does not work quite > as well as `print (fromIntegr 5 :: Int)`, which goes directly to an `Int` > without going through an `Integer` first. I suspect that the reason for > this is that there is some RULE which is not firing, but I'll have to look > into what's going on in a bit more detail. Perhaps Simon has an idea?**** > > ** ** > > -Iavor**** > > ** ** > > ** ** > > On Thu, Aug 23, 2012 at 1:11 AM, Iavor Diatchki < > iavor.diatchki(a)gmail.com> wrote:**** > > Hello,**** > > ** ** > > There are no custom optimizations specifically for type-literals but GHC's > usual optimizations should work well in examples like yours because using a > singleton value is essentially the same as writing the corresponding value > level literal.**** > > So, for example, the indexing function might look something like this:**** > > ** ** > > index :: forall r c a. SingI c => Matrix r c a -> Integer -> Integer > -> a**** > > index (Matrix arr) row col = arr ! (row * fromSing (sing :: Sing c) + > col)**** > > ** ** > > Here, the `SingI` constraint says that we are going to be using the > singleton value associated with type `c`. The function `fromSing` converts > this singleton value into an ordinary `Integer`.**** > > ** ** > > Now, if we use `index` in a context where the dimensions of the matrix are > known, then GHC will resolve the constraint and pass the corresponding > value to `index`. For example, assuming that `index` gets inlined,**** > > the expression:**** > > ** ** > > index (Matrix m :: Matrix 3 4 Int) 1 2**** > > ** ** > > should end up looking something like this:**** > > ** ** > > m ! (1 * 4 + 2)**** > > **** > > which should be simplified further to:**** > > ** ** > > m ! 6 **** > > ** ** > > Does that answer your question? Please ask away if something does not > make sense, or if you notice that things do not work as expected.**** > > ** ** > > Cheers,**** > > -Iavor**** > > ** ** > > On Tue, Aug 21, 2012 at 11:14 AM, Carter Schonwald < > carter.schonwald(a)gmail.com> wrote:**** > > Hey GHC folks!**** > > **** > > In the case where type lits (naturals specifically) are statically known > (rather than abstract), is it possible to have a sort of static copy > propagation / Singelton simplification happen at compile time? (Ie can GHC > do such things with type lits as presently implemented?)**** > > ** ** > > a simple example might be that a statically sized matrix, and being able > to specialize the stride and bounds checking at compile time (pseudo code > example follows)**** > > ** ** > > data Mat (row::Nat) (col::Nat) elem = ... some vector representation**** > > ** ** > > ** ** > > index:: (Mat r c el) -> (Word,Word) -> el**** > > index mt ix = ... some stride based indexing calculation that gets at the > "r" and "c" numbers via the singletons to translate the ix tuple into the > index into the underlying vector**** > > representation**** > > {-# perhaps an inline pragma? #-}**** > > ** ** > > indexSpec3x3:: (Mat 3 3 el) -> (Word, Word) -> el**** > > indexSpec3x3 smat ix = smat `index` ix**** > > ** ** > > under what circumstances can i get something like the body of indexSpec3x3 > to use the static type level natural number machinery to partially > specialize the computation?**** > > Does my question even make sense as phrased?**** > > ** ** > > thanks!**** > > ** ** > > -Carter**** > > ** ** > > ** ** > > ** ** > > ** ** > > _______________________________________________ > Glasgow-haskell-users mailing list > Glasgow-haskell-users(a)haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users**** > > ** ** > > ** ** > > ** ** >

1 0

Comparing StableNames of different type
by Emil Axelsson 28 Aug '12

28 Aug '12

Hi! Are there any dangers in comparing two StableNames of different type? stEq :: StableName a -> StableName b -> Bool stEq a b = a == (unsafeCoerce b) I could guard the coercion by first comparing the type representations, but that would give me a `Typeable` constraint that would spread throughout the code. -- / Emil

5 11

is this a type lits/nats bug or my incorrect understanding ?
by Carter Schonwald 28 Aug '12

28 Aug '12

Hello, I'm trying to understand how much i can build on top of type literals, so as an exercise, i've been trying to see if I can define a type level "absolute different of two natural numbers" i have a minimal example that either type checks in a useless way, or gives a misleading type errors! (or perhaps i am fundamentally not understanding someting) here's the gist for the misleading type error version (it seems to indicate that SingI arity 2, rather than arity 1) https://gist.github.com/3445419 heres the gist for the version that type checks in a useless way! and complains that it doesn't understand that (1<=2) https://gist.github.com/3445456 are these bugs in type nats, or am I missing something? thanks! Carter Schonwald

2 1

I/O overhead in opening and writing files
by J Baptist 28 Aug '12

28 Aug '12

I'm looking into high-performance I/O, particularly on a tmpfs (in-memory) filesystem. This involves creating lots of little files. Unfortunately, it seems that Haskell's performance in this area is not comparable to that of C. I assume that this is because of the overhead involved in opening and closing files. Some cursory profiling confirmed this: most of the runtime of the program is in taken by openFile, hPutStr, and hClose.I thought that it might be faster to call the C library functions exposed as foreign imports in System.Posix.Internals, and thereby cut out some of Haskell's overhead. This indeed improved performance, but the program is still nearly twice as slow as the corresponding C program.I took some benchmarks. I wrote a program to create 500.000 files on a tmpfs filesystem, and write an integer into each of them. I did this in C, using the open; and twice in Haskell, using openFile and c_open. Here are the results:C program, using open and friends (gcc 4.4.3)real 0m4.614suser 0m0.380ssys 0m4.200sHaskell, using System.IO.openFile and friends (ghc 7.4.2)real 0m14.892suser 0m7.700ssys 0m6.890sHaskell, using System.Posix.Internals.c_open and friends (ghc 7.4.2)real 0m7.372suser 0m2.390ssys 0m4.570sWhy question is: why is this so slow? Could the culprit be the marshaling necessary to pass the parameters to the foreign functions? If I'm calling the low-level function c_open anyway, shouldn't performance be closer to C? Does anyone have suggestions for how to improve this?If anyone is interested, I can provide the code I used for these benchmarks.

8 11

7.6.1 RC1 panic "coVarsOfTcCo:Bind"
by Ganesh Sittampalam 24 Aug '12

24 Aug '12

Hi, I'm getting the panic below when building darcs 2.8 with GHC 7.6. It'll take some effort to cut it down or give repro instructions for an uncut-down version (I needed to hack a lot of underlying packages to be able to even get as far as doing this build), so could someone confirm that it's worth it before I do so? I can't spot anything already reporting this in trac. Cheers, Ganesh ghc.exe: panic! (the 'impossible' happened) (GHC version 7.6.0.20120810 for i386-unknown-mingw32): coVarsOfTcCo:Bind cobox{v a6Czs} [lid] = cobox{v a6CTr} [lid] `cast` (<main:Darcs.Test.Patch.WithState.WithState{tc r1LL8} model{tv tC} [tv] (main:Darcs.Witnesses.Ordered.FL{tc r1Dy1} prim{tv ty} [tv] main:Darcs.Witnesses.Ordered.:>{tc r1Dyc} main:Darcs.Witnesses.Ordered.FL{tc r1Dy1} prim{tv ty} [tv])> ghc-prim:GHC.Types.~{(w) tc 31Q} main:Darcs.Test.Patch.WithState.WithState{tc r1LL8} (Sym cobox{v a6CSH} [lid]) <main:Darcs.Witnesses.Ordered.FL{tc r1Dy1} prim{tv ty} [tv] main:Darcs.Witnesses.Ordered.:>{tc r1Dyc} main:Darcs.Witnesses.Order ed.FL{tc r1Dy1} prim{tv ty} [tv]>) Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug

2 2

Problem with default signatures
by Jeroen Weijers 23 Aug '12

23 Aug '12

Hello, I am trying to create some code involving type families and default signatures. I am getting a type error that I do not understand (as far as I can see the error is wrong). I removed all code that doesn't contribute to the error: > {-# LANGUAGE DeriveGeneric, UndecidableInstances, DefaultSignatures, TypeOperators, GADTs, FlexibleContexts, TypeFamilies, FlexibleInstances #-} > module Database.DSH.Problem where > > import GHC.Generics > > data Exp a where > UnitE :: Exp () > ListE :: [Exp a] -> Exp [Exp a] > > class GenericQA f where > type GRep f > type AltGRep f > type AltGRep f = [Exp (GRep f)] > gToExp :: f a -> Exp (GRep f) > emptyAlt :: Exp (AltGRep f) > default emptyAlt :: (AltGRep f ~ [Exp (GRep f)]) => Exp (AltGRep f) > emptyAlt = ListE [] > > instance GenericQA U1 where > type GRep U1 = () > gToExp U1 = UnitE This gives me the following type errors: > Problem.hs:19:10: > Couldn't match type `AltGRep f0' with `[Exp ()]' > Expected type: AltGRep U1 > Actual type: AltGRep f0 > Expected type: Exp (AltGRep U1) > Actual type: Exp (AltGRep f0) > In the expression: (Database.DSH.Problem.$gdmemptyAlt) > In an equation for `emptyAlt': > emptyAlt = (Database.DSH.Problem.$gdmemptyAlt) > > Problem.hs:19:10: > Couldn't match type `GRep f0' with `()' > Expected type: [Exp (GRep f0)] > Actual type: AltGRep f0 > In the expression: (Database.DSH.Problem.$gdmemptyAlt) > In an equation for `emptyAlt': > emptyAlt = (Database.DSH.Problem.$gdmemptyAlt) > In the instance declaration for `GenericQA U1' In this error the type variable f0 is mentioned but as far as I understand it f should have been instantiated to U1 and not to a variable f0. I've tried many variations on the default type signature for emptyAlt but haven't found any that doesn't result in this error. Can somebody explain what is going wrong here? Cheers, Jeroen

2 1

GADTs in the wild
by Simon Peyton-Jones 23 Aug '12

23 Aug '12

Friends I'm giving a series of five lectures at the Laser Summer School<http://laser.inf.ethz.ch/2012/> (2-8 Sept), on "Adventures with types in Haskell". My plan is: 1. Type classes 2. Type families [examples including Repa type tags] 3. GADTs 4. Kind polymorphism 5. System FC and deferred type errors This message is to invite you to send me your favourite example of using a GADT to get the job done. Ideally I'd like to use examples that are (a) realistic, drawn from practice (b) compelling and (c) easy to present without a lot of background. Most academic papers only have rather limited examples, usually eval :: Term t -> t, but I know that GADTs are widely used in practice. Any ideas from your experience, satisfying (a-c)? If so, and you can spare the time, do send me a short write-up. Copy the list, so that we can all benefit. Many thanks Simon

13 23

Fwd: Request for comments on proposal for literate programming using markdown
by Philip Holzenspies 23 Aug '12

23 Aug '12

Below message was rejected because I included the screenshot which was to big. The screenshot referred to is now here: http://tinypic.com/r/2yy6tcy/6 Begin forwarded message: From: "Philip K. F. Hölzenspies" <pkfh(a)st-andrews.ac.uk<mailto:pkfh@st-andrews.ac.uk>> Subject: Re: Request for comments on proposal for literate programming using markdown Date: 22 August 2012 17:36:51 GMT+01:00 To: Nicolas Frisby <nicolas.frisby(a)gmail.com<mailto:nicolas.frisby@gmail.com>> Cc: "glasgow-haskell-users(a)haskell.org<mailto:glasgow-haskell-users@haskell.org>" <glasgow-haskell-users(a)haskell.org<mailto:glasgow-haskell-users@haskell.org>> On 22 Aug 2012, at 17:27, Nicolas Frisby wrote: On Wed, Aug 22, 2012 at 10:02 AM, Nicolas Frisby <nicolas.frisby(a)gmail.com<mailto:nicolas.frisby@gmail.com>> wrote: Maybe just try again in a separate thread? Perhaps under a pseudonym! :) Whoa, just realized once again that email is tone-deaf. I meant that 'pseudonym' thing cheekily: just to help differentiate the proposal in a silly way. In no way was it supposed to be insulting! Sorry for the noise. Tbh, first thing I missed when I saw your mail was not a tonal medium, but a Like button (says something about my cultural deformation, doesn't it ;) I can't speak for others, but I think I read it in the tone you intended.) Also, for the record, I would like for markdown to be an option — regardless of other practical considerations at the moment. It might also be attractive to web people as they check out Haskell. Well, I thought it would be reasonably obvious, but apparently, people like the current output enough to want to keep it. See attached screenshot; this drove me crazy, but that was just me. Ph.

2 1

Re: Request for comments on proposal for literate programming using markdown
by Simon Hengel 22 Aug '12

22 Aug '12

On Thu, Aug 09, 2012 at 01:07:10PM +0000, Philip Holzenspies wrote: > I have looked at pandoc and I use it for quite a few things. Just to clarify, I was not talking about pandoc, but pandoc-unlit (which uses pandoc to unlit Markdown, see the README [1]). > However, it's a bit of an overspec'd package to link into the > compiler, don't you think? I did not mean to modify the Compiler. Unliting is done by an external program. This already allows you to customize unliting [2]. Cheers, Simon [1] https://github.com/sol/pandoc-unlit#readme [2] http://www.haskell.org/ghc/docs/latest/html/users_guide/options-phases.html…

7 20

Long compilation times when profiling a large CAF
by Conal Elliott 22 Aug '12

22 Aug '12

I'm looking for help with crazy-long compile times when using GHC with profiling. A source file at work has a single 10k line top-level definition, which is a CAF. With -prof auto-all or an explicit SCC, compilation runs for 8 hours on a fast machine with the heap growing to 13GB before being killed. Without profiling, it compiles in a few minutes. The big CAFs are auto-generated and not of my making, so I'm hoping for a solution other than "stop making big CAFs". Thanks, -- Conal

2 1