- Haskell-Cafe - Haskell.org

Rigid type-var unification failure in existentials used with parametrically polymorphic functions
by Pablo Nogueira 30 Nov '07

30 Nov '07

A question about existential quantification: Given the existential type: data Box = forall a. B a in other words: -- data Box = B (exists a.a) -- B :: (exists a.a) -> Box I cannot type-check the function: mapBox :: forall a b. (a -> b) -> Box -> Box -- :: forall a b. (a -> b) -> (exists a.a) -> (exists a.a) mapBox f (B x) = B (f x) Nor can I type check: mapBox :: forall a. (a -> a) -> Box -> Box -- :: forall a. (a -> a) -> (exists a.a) -> (exists a.a) mapBox f (B x) = B (f x) The compiler tells me that in both functions, when it encounters the expression |B (f x)|, it cannot unify the universally quantified |a| (which generates a rigid type var) with the existentially quatified |a| (which generates a different rigid type var) -- or so I interpret the error message. However, at first sight |f| is polymorphic so it could be applied to any value, included the value hidden in |Box|. Of course, this works: mapBox :: (forall a b. a -> b) -> Box -> Box mapBox f (B x) = B (f x) Because it's a tautology: given a proof of a -> b for any a or b I can prove Box -> Box. However the only value of type forall a b. a -> b is bottom. This also type-checks: mapBox :: (forall a. a -> a) -> Box -> Box mapBox f (B x) = B (f x) When trying to give an explanation about why one works and the other doesn't, I see that, logically, we have: forall a. P(a) => Q implies (forall a. P(a)) => Q when a does not occur in Q. The proof in our scenario is trivial: p :: (forall a. (a -> a) -> (Box -> Box)) -> (forall a. a -> a) -> Box -> Box p mapBox f b = mapBox f b However, the converse is not true. Yet, could somebody tell me the logical reason for the type-checking error? In other words, how does the unification failure translate logically. Should the first mapBox actually type-check? Isn't the code for mapBox :: forall a. (a -> a) -> Box -> Box encoding the proof: Assume forall a. a -> a Assume exists a.a unpack the existential, x :: a = T for some T apply f to x, we get (f x) :: a pack into existential, B (f x) :: exists a.a Discharge first assumption Discharge second assumption The error must be in step 3. Sorry if this is obvious, it's not to me right now.

3 4

Re: [Haskell-cafe] A tale of Project Euler
by Sebastian Sylvan 30 Nov '07

30 Nov '07

On Nov 28, 2007 12:12 PM, Kalman Noel <kalman.noel(a)bluebottle.com> wrote: > Sebastian Sylvan: > > primes :: [Integer] > > primes = 2 : filter (null . primeFactors) [3,5..] > > > > primeFactors :: Integer-> [Integer] > > primeFactors n = factor n primes > > where > > factor m (p:ps) | p*p > m = [] > > | m `mod` p == 0 = p : factor (m `div` p) (p:ps) > > | otherwise = factor m ps > > Your definition gives a strange meaning to primeFactors. I'd want that for all > n, product (primeFactors n) == n. I think this law holds for the code posted > by Olivier. Yes you're right. That is property should clearly hold. -- Sebastian Sylvan +44(0)7857-300802 UIN: 44640862

9 20

Haskell and DB : giving up
by manu 30 Nov '07

30 Nov '07

Hello I've spent a few days trying to install all the packages required to use HaskellDB with either MySQL or SQlite3 (the only 2 DB the host I was thinking about is supporting) Well, I am giving up ! I seriously regret replacing ghc-6.6 with ghc-6.8, I didn't expect that building packages would be so ... unsucessfull and time-wasting. I just thought I'd let you know what's in store for "PHP-style-users- like-me" who want to use a database with ghc-6.8.1 at the moment, the hurdle is high ! I hope these packages will be fixed soon (I can't figure how to fix them myself obviously). And now I'm going to stay away from my computer for a while :) cheerio M

9 16

Progress indications
by Andrew Coppin 30 Nov '07

30 Nov '07

In a "normal" programming language, you might write something like this: for x = 1 to 1000000 print x ...do slow complex stuff... next x In Haskell, you're more likely to write something like result k = filter my_weird_condition $ map strange_conversion $ unfoldr ... That means that when you try to process the result, lots of processing happens, and your program just appears to lock up until a result is produced. So, like, how do you make it so that some kind of progress information is output while it's working? (Aside from dunking everything into the IO monad and ruining all your beautiful abstractions.) There doesn't seem to be a clean solution to this one...

9 13

Hit a wall with the type system
by Chris Smith 30 Nov '07

30 Nov '07

I was talking to a few people about this on #haskell, and it was suggested I ask here. I should say that I'm playing around here; don't mistake this for an urgent request or a serious problem. Suppose I wanted to implement automatic differentiation of simple functions on real numbers; then I'd take the operations from Num, Fractional, and Floating, and define how to perform them on pairs of values and their differentials, and then I'd write a differentiate function... but finding an appropriate type for that function seems to be a challenge. We have: 1. Differentiating a function of the most general type (Num a => a -> a) should produce a result of type (Num a => a -> a). 2. Differentiating a function of the more specific type (Fractional a => a -> a) should produce a result of that type (Fractional a => a -> a). 3. Differentiating a function of the most specific type (Floating a => a -> a) should produce a result of type (Floating a => a -> a). 4. BUT, differentiating a function which is of a more specific type than (Floating a => a -> a) is not, in general, possible. So differentiate should have type A a => (forall b. A b => b -> b) -> a -> a, but ONLY if the type class A is a superclass of Floating. Two partial solutions are: I can just define the differentiate function for Floating; but that means if I differentiate (\x -> x + 1), the result is a function only on floating point numbers, which is less than desirable. Or, I can define several functions: say, diffNum, diffFractional, and diffFloating... all of which have precisely the same implementation, but different types and require copy/paste to make them work. Any thoughts? For reference, here's the code I kludged together. (Again, I'm only playing around... so I wrote this very quickly and may have gotten some things wrong; don't use my code without checking it first! In particular, I know that this code produces derivative functions whose domain is too large.) > data AD a = AD a a deriving Eq > > instance Show a => Show (AD a) where > show (AD x e) = show x ++ " + " ++ show e ++ " eps" > > instance Num a => Num (AD a) where > (AD x e) + (AD y f) = AD (x + y) (e + f) > (AD x e) - (AD y f) = AD (x - y) (e - f) > (AD x e) * (AD y f) = AD (x * y) (e * y + x * f) > negate (AD x e) = AD (negate x) (negate e) > abs (AD 0 _) = error "not differentiable: |0|" > abs (AD x e) = AD (abs x) (e * signum x) > signum (AD 0 e) = error "not differentiable: signum(0)" > signum (AD x e) = AD (signum x) 0 > fromInteger i = AD (fromInteger i) 0 > > instance Fractional a => Fractional (AD a) where > (AD x e) / (AD y f) = AD (x / y) ((e * y - x * f) / (y * y)) > recip (AD x e) = AD (1 / x) ((-e) / (x * x)) > fromRational x = AD (fromRational x) 0 > > instance Floating a => Floating (AD a) where > pi = AD pi 0 > exp (AD x e) = AD (exp x) (e * exp x) > sqrt (AD x e) = AD (sqrt x) (e / (2 * sqrt x)) > log (AD x e) = AD (log x) (e / x) > (AD x e) ** (AD y f) = AD (x ** y) (e * y * (x ** (y-1)) + > f * (x ** y) * log x) > sin (AD x e) = AD (sin x) (e * cos x) > cos (AD x e) = AD (cos x) (-e * sin x) > asin (AD x e) = AD (asin x) (e / sqrt (1 - x ** 2)) > acos (AD x e) = AD (acos x) (-e / sqrt (1 - x ** 2)) > atan (AD x e) = AD (atan x) (e / (1 + x ** 2)) > sinh (AD x e) = AD (sinh x) (e * cosh x) > cosh (AD x e) = AD (cosh x) (e * sinh x) > asinh (AD x e) = AD (asinh x) (e / sqrt (x^2 + 1)) > acosh (AD x e) = AD (acosh x) (e / sqrt (x^2 - 1)) > atanh (AD x e) = AD (atanh x) (e / (1 - x^2)) > > diffNum :: Num b => (forall a. Num a => a -> a) -> b -> b > diffFractional :: Fractional b => (forall a. Fractional a => a -> a) -> b -> b > diffFloating :: Floating b => (forall a. Floating a => a -> a) -> b -> b > > diffNum f x = let AD y dy = f (AD x 1) in dy > diffFractional f x = let AD y dy = f (AD x 1) in dy > diffFloating f x = let AD y dy = f (AD x 1) in dy -- Chris Smith

8 16

Strings and utf-8
by Maurício 30 Nov '07

30 Nov '07

Hi, Are 'String's in GHC 6.6.1 UTF-8? Thanks, Maurício

11 17

Re: [Haskell-cafe] Re: New slogan for haskell.org
by Ivan Miljenovic 30 Nov '07

30 Nov '07

Speaking of Stackless Python, its homepage (http://www.stackless.com/) has a rather nice layout... maybe slightly less emphasis on the About section, but there you've got the links, the info and the news all on the one page.

3 3

Functional dependencies / monotonic boolean functions in Haskell
by Henning Thielemann 30 Nov '07

30 Nov '07

I know there are Haskell people who are busy with hardware verification and relational algebra. (as indicated by http://www.haskell.org/haskellwiki/Relational_algebra http://www.haskell.org/haskellwiki/Applications_and_libraries/Hardware_veri… ) Is there a Haskell library for working with functional dependencies, namely for computing minimal keys given a set of functional dependencies? Since this problem can also be posed in terms of monotonic boolean functions a library for processing monotonic boolean functions might also help.

1 0

Sillyness in the standard libs.
by Arthur van Leeuwen 29 Nov '07

29 Nov '07

LS, here is a puzzle for you: try converting a System.Posix.Types.EpochTime into either a System.Time.CalendarTime or a Data.Time.Clock.UTCTime without going through read . show or a similar detour through strings. The problem comes up when trying to easily nicely display the access, modification or status change times of a full directory of files, using System.Posix.Files.Filestatus to get at the times. A closely related issue: fromIntegral is in Integral which also requires quotRem. However, the two are semantically quite disjoint. I can *easily* see the semantics of fromIntegral on EpochTime, but not the semantics of quotRem on EpochTime. Having fromIntegral would solve the above puzzle... :) With kind regards, Arthur. -- /\ / | arthurvl(a)cs.uu.nl | Work like you don't need the money /__\ / | A friend is someone with whom | Love like you have never been hurt / \/__ | you can dare to be yourself | Dance like there's nobody watching

7 12

Haskell packaging on Windows "cygwin" (<< POSIX on Windows ; ^)
by Galchin Vasili 29 Nov '07

29 Nov '07

Hello, I trying to get a library to build ... I am following the instructions in http://en.wikibooks.org/wiki/Haskell/Packaging. Under the "Build your project" section in this web page, when I try to do an actual build (runhaskell Setup.lhs build), the imported module System.Environment cannot be found. I suspect that there is a "cygwin" ("Linux/Posix") environment variable that needs to be set to point to the Haskell libraries/packages. ?? Kind regards, Vasya

2 3