Re: [Haskell-cafe] Strange type error with associated type synonyms
On 07/04/2009, Ryan Ingram ryani.s...@gmail.com wrote: On Mon, Apr 6, 2009 at 2:36 PM, Peter Berry pwbe...@gmail.com wrote: As I understand it, the type checker's thought process should be along these lines: 1) the type signature dictates that x has type Memo d a. 2) appl has type Memo d1 a - d1 - a for some d1. 3) we apply appl to x, so Memo d1 a = Memo d a. unify d = d1 This isn't true, though, and for similar reasons why you can't declare a generic instance Fun d = Functor (Memo d). Type synonyms are not injective; you can have two instances that point at the same type: Doh! I'm too used to interpreting words like Memo with an initial capital as constructors, which are injective, when it's really a function, which need not be. You can use a data family instead, and then you get the property you want; if you make Memo a data family, then Memo d1 = Memo d2 does indeed give you d1 = d2. I'm now using Data.MemoTrie, which indeed uses data families, instead of a home-brewed solution, and now GHC accepts the type signature. In fact, it already has a Functor instance, so funmap is redundant. -- Peter Berry pwbe...@gmail.com Please avoid sending me Word or PowerPoint attachments. See http://www.gnu.org/philosophy/no-word-attachments.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Strange type error with associated type synonyms
On Mon, Apr 6, 2009 at 7:39 PM, Manuel M T Chakravarty c...@cse.unsw.edu.au wrote: Peter Berry: 3) we apply appl to x, so Memo d1 a = Memo d a. unify d = d1 But for some reason, step 3 fails. Step 3 is invalid - cf, http://www.haskell.org/pipermail/haskell-cafe/2009-April/059196.html. More generally, the signature of memo_fmap is ambiguous, and hence, correctly rejected. We need to improve the error message, though. Here is a previous discussion of the subject: http://www.mail-archive.com/haskell-cafe@haskell.org/msg39673.html Aha! Very informative, thanks. On 07/04/2009, Manuel M T Chakravarty c...@cse.unsw.edu.au wrote: Matt Morrow: The thing that confuses me about this case is how, if the type sig on memo_fmap is omitted, ghci has no problem with it, and even gives it the type that it rejected: Basically, type checking proceeds in one of two modes: inferring or checking. The former is when there is no signature is given; the latter, if there is a user-supplied signature. GHC can infer ambiguous signatures, but it cannot check them. This is of course very confusing and we need to fix this (by preventing GHC from inferring ambiguous signatures). The issue is also discussed in the mailing list thread I cited in my previous reply. I see. So GHC is wrong to accept memo_fmap? -- Peter Berry pwbe...@gmail.com Please avoid sending me Word or PowerPoint attachments. See http://www.gnu.org/philosophy/no-word-attachments.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Strange type error with associated type synonyms
{-# LANGUAGE TypeFamilies, TypeSynonymInstances, ScopedTypeVariables #-}
The following is a class of memo tries indexed by d:
class Fun d where
type Memo d :: * - *
abst :: (d - a) - Memo d a
appl :: Memo d a - (d - a)
-- Law: abst . appl = id
-- Law: appl . abst = id (denotationally)
Any such type Memo d is naturally a functor:
memo_fmap f x = abst (f . appl x)
The type of memo_fmap (as given by ghci) is (Fun d) = (a - c) -
Memo d a - Memo d c. (Obviously this would also be the type of fmap
for Memo d, so we could declare a Functor instance in principle.) If
we add this signature:
memo_fmap' :: Fun d = (a - b) - Memo d a - Memo d b
memo_fmap' f x = abst (f . appl x)
it doesn't type check:
TypeSynonymTest.hs:14:17:
Couldn't match expected type `Memo d1 b'
against inferred type `Memo d b'
In the expression: abst (f . appl x)
In the definition of `memo_fmap'':
memo_fmap' f x = abst (f . appl x)
TypeSynonymTest.hs:14:32:
Couldn't match expected type `Memo d a'
against inferred type `Memo d1 a'
In the first argument of `appl', namely `x'
In the second argument of `(.)', namely `appl x'
In the first argument of `abst', namely `(f . appl x)'
Failed, modules loaded: none.
As I understand it, the type checker's thought process should be along
these lines:
1) the type signature dictates that x has type Memo d a.
2) appl has type Memo d1 a - d1 - a for some d1.
3) we apply appl to x, so Memo d1 a = Memo d a. unify d = d1
But for some reason, step 3 fails. If we annotate appl with the
correct type (using scoped type variables), it type checks:
-- thanks to mmorrow on #haskell for this
memo_fmap'' :: forall a b d. Fun d = (a - b) - Memo d a - Memo d b
memo_fmap'' f x = abst (f . (appl :: Memo d a - d - a) x)
My ghc is 6.8.2, but apparently this happens in 6.10 as well.
--
Peter Berry pwbe...@gmail.com
Please avoid sending me Word or PowerPoint attachments.
See http://www.gnu.org/philosophy/no-word-attachments.html
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Memoization
Sorry for digging up such an old thread, but my undergraduate dissertation is on this topic so I couldn't resist. :) (Some credit in the following goes to my supervisor, Ulrich Berger.) Mark Engelberg wrote: I'd like to write a memoization utility. Ideally, it would look something like this: memoize :: (a-b) - (a-b) The type you actually want is more like: memoFix :: ((a - b) - a - b) - a - b which is like the normal fixpoint function (defined only over functions) except that it adds the memoization magic. The reason being that you can then memoize recursive calls as well (without having to figure out how to dive into the function definition and replace recursive calls with calls to the memoized version). On 27/05/07, apfelmus [EMAIL PROTECTED] wrote: Note that due to parametricity, any function of this type is necessarily either id or _|_. In other words, there are only two functions of type ∀a∀b. (a-b) - (a-b) Of course, this only talks about the value of id, not its behaviour. fix :: ((a - b) - a - b) - a - b = memoFix in the sense that the values they compute are the same, but practically speaking they are different since the latter does memoization. That's because the functions has to work for all types a and b in the same way, i.e. it may not even inspect how the given types a or b look like. You need type classes to get a reasonable type for the function you want memoize :: Memoizable a = (a-b) - (a-b) Now, how to implement something like this? Of course, one needs a finite map that stores values b for keys of type a. It turns out that such a map can be constructed recursively based on the structure of a: Map ()b := b Map (Either a a') b := (Map a b, Map a' b) Map (a,a')b := Map a (Map a' b) Here, Map a b is the type of a finite map from keys a to values b. Its construction is based on the following laws for functions () - b =~= b (a + a') - b =~= (a - b) x (a' - b) -- = case analysis (a x a') - b =~= a - (a' - b) -- = currying class Memoizable a f | a - f where memIso :: (a - b) :~= f b where a :~= b represents an isomorphism between two types, and f is the generalized trie functor indexed on the type a and storing values of its parameter type (here b). Note that this only works if a is algebraic (i.e. can be represented as a generalized trie using the isomorphisms above and a couple more to deal with recursive and higher kinded types[1]). And it almost goes without saying that you can only memoize pure functions. Then memoFix actually has a constrained type, namely: memoFix :: Memoizable a f = ((a - b) - a - b) - a - b You can then take a recursive function like: f :: A - B f x = ... f y ... and transform it so it takes its own fixpoint as an argument: f' :: (A - B) - A - B f' f x = ... f y ... and then, if you have an instance instance Memoizable A F where memIso = ... after defining F, you can create the memo function with fM : A - B fM = memoFix f' You could generate F and the Memoizable instance using TH or DrIFT or the like (allowing derivation would be really nice :). Actually F could be considered a dependent type, so you could define a pretty much universal instance using TH with that mechanism. For further and detailed explanations, see [1] R. Hinze. Memo functions, polytypically! http://www.informatik.uni-bonn.de/~ralf/publications.html#P11 and R. Hinze. Generalizing generalized tries. http://www.informatik.uni-bonn.de/~ralf/publications.html#J4 also: T. Altenkirch. Representations of first order function types as terminal coalgebras. http://www.cs.nott.ac.uk/~txa/publ/tlca01a.pdf which unfortunately you probably won't understand unless you know about category/domain theory (I haven't figured it all out myself). -- Peter Berry [EMAIL PROTECTED] Please avoid sending me Word or PowerPoint attachments. See http://www.gnu.org/philosophy/no-word-attachments.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Memoization
On 08/06/07, Peter Berry [EMAIL PROTECTED] wrote: You could generate F and the Memoizable instance using TH or DrIFT or the like (allowing derivation would be really nice :). Actually F could be considered a dependent type, so you could define a pretty much universal instance using TH with that mechanism. I meant associated type of course. -- Peter Berry [EMAIL PROTECTED] Please avoid sending me Word or PowerPoint attachments. See http://www.gnu.org/philosophy/no-word-attachments.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] type inference futility
On 16/04/07, Paul Wankadia [EMAIL PROTECTED] wrote: Is it impossible for the compiler to infer the type from the methods called? Your code: main :: IO () main = do x - new From the use of 'new', the compiler can infer that the type of x is an instance of MehBase, and... shift x from the use of 'shift', that it is an instance of HasShift. return () So we have x :: (MehBase a, HasShift a) = a. There isn't enough information provided to pin down 'a' any more precisely, so GHC can't figure out which 'new' or 'shift' you mean (remember that type classes provide overloading), and gives up. There is one special case where the compiler does infer a specific type despite not having enough information to do so, and that is where the class(es) is/are numeric. For example (Floating a) = a might default to Float or Double. This is one case where the compiler decides it can make 'reasonable' assumptions as to what you actually wanted. It's also why ambiguous types seem to work in the interpreter, if you've only ever looked at numeric ones. In the case of the code you posted, GHC isn't smart enough to realise that there's only one type in scope that satisfies the constraints. Here's the relevant part of the report: http://www.haskell.org/onlinereport/decls.html#sect4.3.4 Felipe's suggestion is probably the best way to fix it, i.e. tell the compiler exactly which type you want. The report seems to suggest you can give the compiler a list of defaults in the module declaration but I don't know if that would be sensible. -- Peter Berry [EMAIL PROTECTED] Please avoid sending me Word or PowerPoint attachments. See http://www.gnu.org/philosophy/no-word-attachments.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Fwd: [Haskell-cafe] Newbie: generating a truth table
Sigh, I seem to have done a reply to sender. Reposting to the list. On 06/02/07, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote: Hello, I would like to create a Haskell function that generates a truth table, for all Boolean values, say, using the following and function : and :: Bool - Bool - Bool and a b = a b A fairly old thread, but I had an interesting idea: combos :: (Enum a, Enum b) = a - b - (a - b - c) - [(a, b, c)] combos min1 min2 op = [(x, y, x `op` y) | x - [min1..], y - [min2..]] Then: *Main combos False () [(False,False,False),(False,True,False),(True,False,False),(True,True,True)] In the case of Bool and a few others, you can use a slightly nicer one: bCombos :: (Enum a, Bounded a, Enum b, Bounded b) = (a - b - c) - [(a, b, c)] bCombos op = [(x, y, x `op` y) | x - [minBound..maxBound], y - [minBound..maxBound]] And: *Main bCombos () [(False,False,False),(False,True,False),(True,False,False),(True,True,True)] The secret of these is of course in the Enum and Bounded type classes, which define, respectively, * enumFrom and enumFromTo (which have syntactic sugar in [foo..] and [foo..bar] respectively), and * minBound and maxBound. You can do the same with any instance of these classes. -- Peter Berry [EMAIL PROTECTED] Please avoid sending me Word or PowerPoint attachments. See http://www.gnu.org/philosophy/no-word-attachments.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Fwd: [Haskell-cafe] Optimization fun
Gah! Gmail has really broken defaults for posting to lists. On 10/02/07, Creighton Hogg [EMAIL PROTECTED] wrote: Hello Haskell-ers, So a friend and I were thinking about making code faster in Haskell, and I was wondering if there was a way to improve the following method of generating the list of all prime numbers. It takes about 13 seconds to run, meanwhile my friend's C version took 0.1. I'd love to learn a bit more about how to optimize Haskell code. Which subproblem takes 13 seconds? (Surely generating a list of all primes will take an infinite amount of time, since there are infinitely many of them?) -- Peter Berry [EMAIL PROTECTED] Please avoid sending me Word or PowerPoint attachments. See http://www.gnu.org/philosophy/no-word-attachments.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Currying
On 18/01/07, Chris Eidhof [EMAIL PROTECTED] wrote: That's exactly what I love about haskell: it saves me from a lot of unnecessary typing. After all, I'm a lazy programmer ;) Lazy languages for lazy programmers 8) On 18/1/2007, Johan Grönqvist [EMAIL PROTECTED] wrote: add x y = x + y map (add 2) [1..5] Don't know if you know this, but infix operators like (+) are functions too, and you can partially apply them using 'sections': map (+2) [1..5] It's only syntax, but this is one of the things I really like about Haskell. -- Peter Berry [EMAIL PROTECTED] Please avoid sending me Word or PowerPoint attachments. See http://www.gnu.org/philosophy/no-word-attachments.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Haskell category (was: Article review: Category Theory)
On 16/01/07, David House [EMAIL PROTECTED] wrote: I'd love comments from newcomers and experts alike regarding my approach, the content, improvements and so on. Of course, it's on the wikibook, so if you have anything to add (that's not _too_ substantial otherwise I'd recommend discussion first) then go ahead. Interesting timing for me :) I was going to post about category theory as well, but my motivation is the opposite - I'd like to ask about it. (I've changed the subject since this ought to be a separate thread.) My final year undergraduate project involves defining the semantics of a memoization function in Haskell using category theory, so of course I've been trying to figure out exactly what the Haskell category consists of. I've put a summary of my thoughts at http://sucs.org/~pwb/cats.txt . I'd appreciate comments, criticism, etc. -- Peter Berry [EMAIL PROTECTED] Please avoid sending me Word or PowerPoint attachments. See http://www.gnu.org/philosophy/no-word-attachments.html ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
