May 2010 - Haskell-Cafe

Help with Bird problem 3.3.3
by Peter Hilal 11 Jun '10

11 Jun '10

I'm working my way through Bird's _Introduction to Functional Programming Using Haskell_. I'd appreciate any help with problem 3.3.3, which is: "Division of natural numbers can be specified by the condition (n * m) / n = m for all positive n and all m. Construct a program for division and prove that it meets the specification." The required construction relies on the following definitions: data Nat = Zero| Succ Nat (+) :: Nat -> Nat m + Zero = m m + Succ n = Succ (m + n) (*) :: Nat -> Nat m * Zero = Zero m * Succ n = m * n + m Proceeding as Bird does in Sec. 3.2.2, where he derives the definition of "-" from the specification "(m + n) - n = m", I've so far gotten the first case, in which m matches the pattern "Zero", simply by (i) substituting Zero for m in the specification, (ii) substituting Succ n for n in the specification (solely because n is constrained to be positive), and (iii) reducing by applying the first equation of "*": Case Zero: (Succ n * Zero) / Succ n = Zero ≡ {first equation of "*"} Zero / Succ n = Zero Easy enough, and completely intuitive, since we expect Zero divided by any non-Zero finite number to be Zero. The next case, in which m matches the pattern "Succ m", is where I get stuck, and I really have no intuition about what the definition is supposed to be. My first step is to substitute "Succ m" for "m" in the given specification, and to substitute Succ n for n in the specification (for the same reason, as above, that n is constrained to be positive), and then to use the definition of "*" to reduce the equation: Case Succ m: Succ n * Succ m / Succ n = Succ m ≡ {second equation of "*"} (Succ n * m + Succ n) / Succ n = Succ m Where do I go from here? Thank you so much.

5 4

Proposal to solve Haskell's MPTC dilemma
by Carlos Camarao 09 Jun '10

09 Jun '10

This message presents, informally, a proposal to solve Haskell's MPTC (multi-parameter type class) dilemma. If this informal proposal turns out to be acceptable, we (I am a volunteer) can proceed and make a concrete proposal. The proposal has been published in the SBLP'2009 proceedings and is available at www.dcc.ufmg.br/~camarao/CT/solution-to-MPTC-dilemma.pdf The well-known dilemma (hackage.haskell.org/trac/haskell-prime/wiki/MultiParamTypeClassesDilemma) is that it is generally accepted that MPTCs are very useful, but their introduction is thought to require the introduction also of FDs (Functional Dependencies) or another mechanism like ATs (Associated Types) and FDs are tricky and ATs, somewhat in a similar situation, have been defined more recently and there is less experience with its use. In www.haskell.org/ghc/dist/current/docs/html/users_guide/type-class-extension… there exists a solution to the termination problem related to the introduction of MPTCs in Haskell. In our proposal, neither FDs nor any other mechanism like ATs are needed in order to introduce MPTCs in Haskell; the only change we have to make is in the ambiguity rule. This is explained below. The termination problem is essentially ortogonal and can be dealt with, with minor changes, as described in the solution presented in the above mentioned (type-class-extensions) web page. Let us review the ambiguity rule used in Haskell-98 and after that the ambiguity rule used in GHC. Haskell-98 ambiguity rule (which is adequate for Haskell-98's single parameter type classes) is: a type C => T is ambiguous iff there is a type variable v that occurs in the "context" (constraint set) C but not in the simple (unconstrained) type T. For example: forall a.(Show a, Read a)=>String is ambiguous, because "a" occurs in the constraints (Show a,Read a) but not in the simple type (String). In the context of MPTCs, this rule alone is not enough. Consider, for example (Example 1): class F a b where f:: a->b class O a where o:: a and k = f o:: (C a b,O a) => b Type forall a b. (C a b,O a) => b can be considered to be not ambiguos, since overloading resolution can be defined so that instantiation of "b" can "determine" that "a" should also be instantiated (as FD b|->a does), thus resolving the overloading. GHC, since at least version 6.8, makes significant progress towards a definition of ambiguity in the context of MPTCs; GHC 6.10.3 Users Guide says (section 7.8.1.1): "GHC imposes the following restrictions on the constraints in a type signature. Consider the type: forall tv1..tvn (c1, ...,cn) => type. ... Each universally quantified type variable tvi must be reachable from type. A type variable a is reachable if it appears in the same constraint as either a type variable free in the type, or another reachable type variable. For example, type variable "a" in constraint (O a) in the example above is reachable, because it appears in (C a b) (the same constraint as type variable "b", which occurs in the simple type). Our proposal is: consider unreachability not as indication of ambiguity but as a condition to trigger overloading resolution (in a similar way that FDs trigger overloading resolution): when there is at least one unreachable variable and overloading is found not to be resolved, then we have ambiguity. Overloading is resolved iff there is a unique substitution that can be used to specialize the constraint set to one, available in the current context, such that the specialized constraint does not contain unreachable type variables. (A formal definition, with full details, is in the cited SBLP'09 paper.) Consider, in Example 1, that we have a single instance of F and O, say: instance F Bool Bool where f = not instance O Bool where o = True and consider also that "k" is used as in e.g.: kb = not k According to our proposal, kb is well-typed. Its type is Bool. This occurs because (F a b, O a)=>Bool can be simplified to Bool, since there exists a single substitution that unifies the constraints with instances (F Bool Bool) and (O Bool) available in the current context, namely S = (a|->Bool,b|->Bool). As another example (Example 2), consider: {-# NoMonomorphismRestriction, MultiParameterTypeClasses #-} data Matrix = ... data Vector = ... class Mult a b c where (*):: a ! b ! c instance Mult Matrix Vector Matrix where (*) = ... instance Mult Matrix Vector Vector where (*) = ... m1:: Matrix = ... m2:: Vector = ... m3:: Vector = ... m = (m1 * m2) * m3 GHC gives the following type to m: m :: forall a, b. (Mult Matrix Vector a, Mult a Vector b) => b However, "m" cannot be used effectively in a program compiled with GHC: if we annotate m::Matrix, a type error is reported. This occurs because the type inferred for "m" includes constraints (Mult Matrix Vector a, Mult a Vector Matrix) and, with b|->Matrix, type variable "a" appears only in the constraint set, and this type is considered ambiguous. Similarly, if "m" is annotated with type Vector, the type is also considered ambiguous. There is no means of specializing type variable "a" occurring in the type of "m" to Matrix. And no FD may be used in order to achieve such specialization, because we do not have here a FD: "a" and "b" do not determine "c" in class Mult: for (a,b = Matrix,Vector), we can have "c" equal to either Matrix or Vector. According to our proposal, type m:: forall a. (Mult Matrix Vector a, Mult a Vector Matrix)) => Matrix is not ambiguous, in the context of the class and instance declarations of Example 2 (since "a" can be instantiated to Matrix), whereas type m:: forall a.(Mult Matrix Vector a, Mult a Vector Matrix)) => Vector is ambiguous in this context. We would like to encourage compiler front-end developers to change Haskell's ambiguity rule, and test with as many examples as desired, including recurring examples that appear in Haskell mailing lists involving MPTCs, FDs etc. We would like to hear and discuss your doubts, opinions, comments, criticisms etc. Cheers, Carlos

10 20

A question on existential types and Church encoding
by Cory Knapp 08 Jun '10

08 Jun '10

Hello, A professor of mine was recently playing around during a lecture with Church booleans (I.e., true = \x y -> x; false = \x y -> y) in Scala and OCaml. I missed what he did, so I reworked it in Haskell and got this: >type CB a = a -> a -> a >ct :: CB aC >ct x y = x >cf :: CB a >cf x y = y >cand :: CB (CB a) -> CB a -> CB a >cand p q = p q cf >cor :: CB (CB a) -> CB a -> CB a >cor p q = p ct q I found the lack of type symmetry (the fact that the predicate arguments don't have the same time) somewhat disturbing, so I tried to find a way to fix it. I remembered reading about existential types being used for similar type-hackery, so I added quantification to the CB type and got >type CB a = forall a . a -> a -> a >ctrue :: CB a >ctrue x y = x >cfalse :: CB a >cfalse x y = y >cand :: CB a -> CB a -> CB a >cand p q = p q cfalse >cor :: CB a -> CB a -> CB a >cor p q = p ctrue q which works. But I haven't the faintest idea why that "forall" in the type makes things work... I just don't fully understand existential type quantification. Could anyone explain to me what's going on that makes the second code work? Thanks, Cory

7 10

RE: [Haskell-cafe] GHC Api typechecking
by Phyx 07 Jun '10

07 Jun '10

Hi, I checked out how Hint is doing it, but unfortunately they're calling a function in the GHC api's interactive part to typecheck a single statement, much like :t in ghci, So I can't use it to typecheck whole modules. I've tried working around not being able to construct a TargetId but ran into another wall. I can't find anyway to do dependency analysis on the in-memory target, so the dependency graph would be empty which is ofcourse a big problem. Does anyone know if Leksah uses the GHC api for typechecking? And if it only gives type errors after you save a file? The code I've been trying is typeCheckStringOnly :: String -> IO (ApiResults Bool) typeCheckStringOnly contents = handleSourceError processErrors $ runGhc (Just libdir) $ do buffer <- liftIO $ stringToStringBuffer contents clock <- liftIO getClockTime dflags <- getSessionDynFlags setSessionDynFlags dflags let srcLoc = mkSrcLoc (mkFastString "internal:string") 1 1 dynFlag = defaultDynFlags state = mkPState buffer srcLoc dynFlag parsed = unP Parser.parseModule state pkgId = stringToPackageId "internal" name = mkModuleName "Unknown" mod' = mkModule pkgId name location = ModLocation Nothing "" "" summary = ModSummary mod' HsSrcFile location clock Nothing [] [] "" dynFlag Nothing (\a->setSession $ a { hsc_mod_graph = [summary] }) =<< getSession case parsed of PFailed _ _ -> return $ ApiOk False POk newstate mdata -> do let module' = ParsedModule summary mdata check <- typecheckModule module' return $ ApiOk True this fails with a ghc panic : panic! (the 'impossible' happened) (GHC version 6.12.1 for i386-unknown-mingw32): no package state yet: call GHC.setSessionDynFlags Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug :( Cheers, Phyx -----Original Message----- From: Gwern Branwen [mailto:gwern0@gmail.com] Sent: Saturday, April 17, 2010 20:59 To: Phyx Subject: Re: [Haskell-cafe] GHC Api typechecking On Sat, Apr 17, 2010 at 1:49 PM, Phyx <lonetiger(a)gmail.com> wrote: > Hi all, I was wondering if someone knows how to do the following: > > > > I’m looking to typecheck a string using the GHC Api, where I run into > problems is that I need to construct a Target, but the TargetId only seem to > reference physical files. > > > > Ofcourse I can write the string to a file and typecheck that file, but I > would like to do it all in memory and avoid IO if possible. > > > > Does anyone know if this is possible? > > > > For the record I’m trying to create the target as follows > > > > createTarget :: String -> IO Target > > createTarget content = > > do clock <- getClockTime > > buffer <- stringToStringBuffer content > > return $ Target { targetId = TargetModule (mkModuleName > "string:internal") ß problem > > , targetAllowObjCode = True > > , targetContents = Just (buffer,clock) > > } > > > > typeCheckStringOnly :: String -> IO (ApiResults Bool) > > typeCheckStringOnly contents = handleSourceError processErrors $ > > runGhc (Just libdir) $ do > > dflags <- getSessionDynFlags > > setSessionDynFlags dflags > > target <- liftIO $ createTarget contents > > addTarget target > > load LoadAllTargets > > let modName = mkModuleName "string:internal" ß problem again, don’t know > how to create the dependency graph then. > > graph <- depanal [modName] True > > (\a->setSession $ a { hsc_mod_graph = graph }) =<< getSession > > value <- fmap typecheckedSource (typeCheck modName) > > return $ ApiOk True > > > > Cheers, > > Phyx Have you looked at how the Hint package does things? -- gwern

2 3

Difference between div and /
by Maciej Piechotka 05 Jun '10

05 Jun '10

I started to wonder what is the difference between div and / so they are 2 separate symbols. div: Take a Integral divide and round (down) (/): Take a Fractional divide and usually round In some applications I would like to use any of those but it is not possible. Is this unification taken into account while reworking numeric classes? I.e. why not: class Num a => Divisable a where (/) :: a -> a -> a class (Real a, Enum a, Divisable a) => Integral a where quot :: a -> a -> a rem :: a -> a -> a div = (/) mod :: a -> a -> a x `quotRem` y = (x `quot` y, x `rem y) x `divMod` y = (x `div` y, x `mod` y) toInteger :: a -> Integer class Divisable a => Fractional a where recip = (1/) :: a -> a fromRational :: Rational -> a (Example does not take into account other refactoring) Regards PS. Why is Fd/cPid etc. Integral or even Num? What does (stdin + stderr) `mod` stdout mean (result will be stdin).

10 23

Problems with Haskell Platform
by Dominic Steintiz 05 Jun '10

05 Jun '10

I seem to be in some sort package dependency hell (which I thought the Haskell Platform did away with). I install ghc using my package manager (I'm on opensuse). > dom1@fourier:~> ghc --version > The Glorious Glasgow Haskell Compilation System, version 6.12.1 > dom1@fourier:~> cabal --version > cabal-install version 0.8.2 > using version 1.8.0.4 of the Cabal library > dom1@fourier:~> cabal update > Downloading the latest package list from hackage.haskell.org But > dom1@fourier:~> cabal upgrade cabal-install > Resolving dependencies... > Downloading HTTP-4000.0.9... > Configuring HTTP-4000.0.9... > Preprocessing library HTTP-4000.0.9... > Building HTTP-4000.0.9... > > Network/StreamSocket.hs:30:7: > Could not find module `Network.Socket': > There are files missing in the `network-2.2.1.7' package, > try running 'ghc-pkg check'. > Use -v to see a list of the files searched for. > cabal: Error: some packages failed to install: > HTTP-4000.0.9 failed during the building phase. The exception was: > ExitFailure 1 > cabal-install-0.8.2 depends on HTTP-4000.0.9 which failed to install. And trying to install the Haskell Platform via http://hackage.haskell.org/platform/2010.1.0.0/cabal/haskell-platform-2010.… > dom1@fourier:~> cabal install > Resolving dependencies... > cabal: dependencies conflict: ghc-6.12.1 requires directory ==1.0.1.1 > however > directory-1.0.1.1 was excluded because ghc-6.12.1 requires directory > ==1.0.1.0 Which is somewhat baffling. So I uninstalled ghc via the package manager and downloaded the linux binaries at http://haskell.org/ghc/dist/6.12.1/ghc-6.12.1-i386-unknown-linux-n.tar.bz2 But sadly > dom1@fourier:~/Downloads/ghc-6.12.1> ./configure > checking for path to top of build tree... ./configure: line 1687: > utils/ghc-pwd/ghc-pwd: cannot execute binary file > configure: error: cannot determine current directory And indeed it is true > dom1@fourier:~/Downloads/ghc-6.12.1> utils/ghc-pwd/ghc-pwd > bash: utils/ghc-pwd/ghc-pwd: cannot execute binary file I'm not sure where to go from here. I think my options are a) build ghc from source or b) find the source for ghc-pwd and compile it and then try configure again. Any help would be appreciated. Dominic.

9 19

The state of Hackage: what are we doing about it?
by Don Stewart 03 Jun '10

03 Jun '10

I see fairly regular complaints about too many Haskell libraries, bewildering choice of difficult-to-determine quality. I've tried to summarize the state of Hackage, and what projects are active to make it easier to find high quality libraries: http://tinyurl.com/2cqw9sb Thoughts? -- Don

10 17

Wire GUI
by Andrew Coppin 03 Jun '10

03 Jun '10

I'm looking at a project which involves a GUI where you can insert components and wire up connections between them. Obviously the details of what the components are and what code gets executed for them is domain-specific, however the general idea of graphically wiring things together is quite generic. Has anybody already put together a Haskell library for doing this kind of thing?

6 7

How to build an "Indicator Type" for a type class?
by Steffen Schuldenzucker 03 Jun '10

03 Jun '10

Dear Cafe, let: > data True > data False > > class C a (arbitrary instances for C may follow) Now, how to obtain an "Indicator Type" for C, i.e. a type IndC that is defined via a type family / fundep / ... , so that IndC a = True forall a which are instances of C IndC a = False for all other a. I've collected some failed approaches here[1]. My key problem is that if I define (in the 3rd try): > instance (C a) => IndC3 a True , it does *not* mean "Define this instance for all a which are an instance of C", but "Define the instance IndC3 a True for all types a, but it's not gonna work if a is not an instance of C". Does anyone have another idea? Background: After having implemented type-level lists[2] and a quicksort on them[3], I'd like to have type-level sets. In their most simple implementation, sets are just (unsorted) lists like this: > data Nil > data Cons a b > class Elem x l (instances for Elem so that Elem x l iff x is an element of the list l) Now I want: > type family Insert x s :: * Insert x s = s forall (x, s) with (Elem x s) Insert x s = Cons x s for all other (x, s). Thanks a lot! Steffen [1] http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25832#a25832 [2] Kiselyov, Peyton-Jones, Shan: "Fun with type functions" http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/fu… [3] I rewrote this algorithm using type families instead of fundeps: http://www.haskell.org/haskellwiki/Type_arithmetic#An_Advanced_Example_:_Ty…

2 2

Re: [web-devel] Google Summer of Code: BlazeHTML RFC
by Matt Parker 02 Jun '10

02 Jun '10

> Q3: Which HTML version would you preferably use? > HTML 5. google summer of code should be about pushing the new and exciting.

7 8