Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Getting a value of type Integral a => [a] from a value of Integral a => ([a],[a],[a])

Tags:

haskell

So I'm playing around with this:

factors :: Integral a => a -> [a] 
factors n = filter (\d -> n `rem` d == 0) . takeWhile (\d -> d*d <= n) $ [ 1 .. ]

abundants_perfects_deficients :: Integral a => ([a],[a],[a])
abundants_perfects_deficients = foldr switch ([],[],[]) [1..]
  where switch :: Integral a => a -> ([a],[a],[a]) -> ([a],[a],[a])
        switch n (as,ps,ds) = 
          let t = sum (factors n) in
                if t < n  then  (as,ps,n:ds) 
          else  if t == n then  (as,n:ps,ds) 
          else                  (n:as,ps,ds)

And while I've got abundants_perfects_deficients, I'd rather have three values: abundants, perfects, and deficients all of type Integral a -> [a].

One thing that doesn't work is:

abundants,perfects,deficients :: Integral a => [a] 
(abundants,perfects,deficients) = abundants_perfects_deficients

Because this constrains the three to all be over the same a.

I tried something to do them one-by-one, so they wouldn't mutually constrain, but that didn't work either:

perfects :: Integral a => [a] 
(_,perfects,_) = abundants_perfects_deficients

Because the compiler couldn't figure out how to convert a value of type forall a. Integral a => ([a],[a],[a]) to type (t1, forall a. Integral a => [a], t2).

Which seems cromulent enough.

Now I know I could implement them separately (just perfects = filter isPerfect [1..]), or constrain them to all be of the same type ((abundants,perfects,deficients) = abundants_perfects_deficients works fine if abundants,perfects,deficients :: [Integer]), but

  • I like using the shared information to build all three
  • I want to not just be constrained to Integers

ideas?


Edit: Fascinatingly enough this works:

abundants :: Integral a => [a]
abundants = f as
  where as :: [Integer]
        (as,_,_) = abundants_perfects_deficients
        f :: Integral a => [Integer] -> [a]
        f = map fromInteger

But this doesn't:

abundants_perfects_deficients' :: (Integral a,Integral p, Integral d) => ([a],[p],[d])
abundants_perfects_deficients' = (f as, f ps, f ds)
  where as,ps,ds :: [Integer]
        (as,ps,ds) = abundants_perfects_deficients
        f :: Integral a => [Integer] -> [a]
        f = map fromInteger

abundants,perfects,deficients :: (Integral a) => [a]
(abundants,perfects,deficients) = abundants_perfects_deficients'

I have no idea why.

like image 275
rampion Avatar asked Sep 19 '11 15:09

rampion


1 Answers

This relates to what polymorphic types really mean, which is slightly more complicated than how they first appear.

At this point it's probably easier to switch modes of thinking and look at the quantifier as being a form of lambda abstraction: A type like ∀ a. [a] is thus a function taking a single type argument, and returning a list of things of that type. Class constraints like Integral a can be seen as additional arguments (specifically, the instance dictionary) which are implicitly provided when GHC finds the values for you.

To emphasize the point, I'm going to write the quantifiers as /\ a -> to mimic lambda syntax, and write class constraints as regular arguments.

Written this way, the type of abundants_perfects_deficients is /\a -> Integral a -> ([a],[a],[a]), and your initial attempt failed essentially because you were trying to pattern match on the result of a two-argument function. In many cases GHC automagically shuffles these implicit arguments around to make things work out, but here it quite clearly can't--to get any result from abundants_perfects_deficients you first need to apply it to both arguments, getting a monomorphic result, which is then bound using the pattern. Even when the pattern binds only one value, the rest being _, GHC still needs to type-check the pattern binding itself, so even though it seems like the extra arguments could be floated out to the single bound identifier, this fails for the same reason as binding all three at once.

To bind three polymorphic values with a pattern, you would instead need the extra arguments to be on the inside, giving abundants_perfects_deficients a type like (/\a -> Integral a -> [a], /\a -> Integral a -> [a], /\a -> Integral a -> [a]). This requires the ImpredicativeTypes extension, which has a somewhat checkered past, and which I'm still wary of.

A lot of what's tripping you up here is that GHC isn't clever enough to figure out "obvious" things, like floating implicit type and constraint arguments based on only being used within a particular part of a binding. Given how much magic it already does behind the scenes, this doesn't bother me too much. :]

The simplest solution is to just bind all three separately, using a selection function to extract the individual elements. This lets the top-level binding be polymorphic in the expected way, with the implicit arguments it receives implicitly passed along to abundants_perfects_deficients, and the projection function simply discarding the other three after a (now monomorphic) pattern match.

like image 181
C. A. McCann Avatar answered Sep 21 '22 01:09

C. A. McCann