Re: Untouchable type variables

This doesn't sound like the right explanation to me. Untouchable variables don't have anything (necessarily) to do with existential quantification. What they have to do with is GHC's (equality) constraint solving. I don't completely understand the algorithm. However, from what I've read and seen

Re: TDNR without new operators or syntax changes

On Thu, May 26, 2016 at 5:14 AM, Peter wrote: > Solving for everything but f, we get f :: T -> Int. So TDNR happens for things in function position (applied to something). > Solving for everything but f, we get f :: T -> Int. So TDNR happens for things in argument

Re: TDNR without new operators or syntax changes

As a supplement, here's a series of definitions to think about. The question is: what should happen in each section, and why? The more detailed the answer, the better. Definitions from previous sections are in scope in subsequent ones, for convenience. The examples are arranged in a slippery

Re: suboptimal ghc code generation in IO vs equivalent pure code case

On Tue, May 10, 2016 at 4:45 AM, Harendra Kumar wrote: > Thanks Dan, that helped. I did notice and suspect the update frame and the > unboxed tuple but given my limited knowledge about ghc/core/stg/cmm I was > not sure what is going on. In fact I thought that the

Re: suboptimal ghc code generation in IO vs equivalent pure code case

I'm no expert on reading GHC's generated assembly. However, there may be a line you've overlooked in explaining the difference, namely: movq $stg_upd_frame_info,-16(%rbp) This appears only in the IO code, according to what you've pasted, and it appears to be pushing an update frame (I

Re: Breaking Changes and Long Term Support Haskell

not because of the technical decisions that are > being made, but because of the process by which they are being made. > That concern is what drove my proposals. It is perfectly valid to think > that that loss was the inevitable price of progress, but that is not my > view. > > Cheers,

Re: Breaking Changes and Long Term Support Haskell

Hello, I'm Dan Doel. I'm on the core libraries committee (though I'm speaking only for myself). As I recall, one of the reasons I got tapped for it was due to my having some historical knowledge about Haskell; not because I was there, but because I've gone back and looked at some old reports

Re: Closed Type Families: type checking dumbness? [was: separate instance groups]

It seems to me the problem is that there's no way to define classes by consecutive cases to match the family definitions. I don't know what a good syntax for that would be, since 'where' syntax is taken for those. But it seems like it would correspond fill the hole here. On Sun, Jun 7, 2015 at

Re: [Haskell-cafe] RFC: Native -XCPP Proposal

vector generates a considerable amount of code using CPP macros. And with regard to other mails, I'm not too eager (personally) to port that to template Haskell, even though I'm no fan of CPP. The code generation being done is so dumb that CPP is pretty much perfect for it, and TH would probably

Re: Increased memory usage with GHC 7.10.1

You aren't the only one. The vector test suite also has these kind of issues. In its case, it's hard for me to tell how big the code is, because template haskell is being used to generate it. However, I don't think the template haskell is what's using the additional performance, because the test

Re: [Haskell] Rank-N types with (.) composition

Impredicativity, with regard to type theories, generally refers to types being able to quantify over the collection of types that they are then a part of. So, the judgment: (forall (a :: *). a - a) :: * is impredicative, because we have a type in * that quantifies over all types in *, which

Re: [Haskell] Rank-N types with (.) composition

a similar rule, like: Whenever you see: f Prelude.. g instead try to type check: \x - f (g x) -- Dan On Tue, Feb 10, 2015 at 6:19 PM, Tyson Whitehead twhiteh...@gmail.com wrote: On February 10, 2015 16:28:56 Dan Doel wrote: Impredicativity, with regard to type theories, generally refers

Re: Proposal: ValidateMonoLiterals - Initial bikeshed discussion

Assuming a separate syntax, I believe that the criterion would be as simple as ensuring that no ValidateFoo constraints are left outstanding. The syntax would add the relevant validate call, and type variables involved in a ValidateFoo constraint would not be generalizable, and would have to be

Re: Overlapping and incoherent instances

On Mon, Aug 11, 2014 at 11:36 AM, Twan van Laarhoven twa...@gmail.com wrote: To me, perhaps naively, IncoherentInstances is way more scary than OverlappingInstances. ​It might be a bit naive. Most things that incoherent instances would allow are allowed with overlapping instances so long as

Re: Bang Patterns

Filed. Bug #8952. On Wed, Apr 2, 2014 at 3:41 PM, wren romano winterkonin...@gmail.comwrote: On Tue, Apr 1, 2014 at 3:02 PM, Dan Doel dan.d...@gmail.com wrote: Specifically, consider: case Nothing of !(~(Just x)) - 5 Nothing - 12 Now, the way I'd expect

Eta Reduction

In the past year or two, there have been multiple performance problems in various areas related to the fact that lambda abstraction is not free, though we tend to think of it as so. A major example of this was deriving of Functor. If we were to derive Functor for lists, we would end up with

Bang Patterns

Greetings, I've been thinking about bang patterns as part of implementing our own Haskell-like compiler here, and have been testing out GHC's implementation to see how it works. I've come to one case that seems like it doesn't work how I think it should, or how it is described, and wanted to ask

Re: Desugaring do-notation to Applicative

Unfortunately, in some cases, function application is just worse. For instance, when the result is a complex arithmetic expression: do x - expr1; y - expr2; z - expr3; return $ x*y + y*z + z*x In cases like this, you have pretty much no choice but to name intermediate variables, because the

Re: [Haskell-cafe] ScopedTypeVariables

This is already a separate extension: PatternSignatures. However, that extension is deprecated for some reason. On Tue, Aug 6, 2013 at 2:46 PM, Evan Laforge qdun...@gmail.com wrote: Occasionally I have to explicitly add a type annotation, either for clarity or to help choose a typeclass

Re: [Haskell-cafe] ScopedTypeVariables

This is already a separate extension: PatternSignatures. However, that extension is deprecated for some reason. On Tue, Aug 6, 2013 at 2:46 PM, Evan Laforge qdun...@gmail.com wrote: Occasionally I have to explicitly add a type annotation, either for clarity or to help choose a typeclass

Re: Proposal: Non-recursive let

On Wed, Jul 10, 2013 at 3:08 AM, Andreas Abel andreas.a...@ifi.lmu.dewrote: Another instance (cut-down) are let-guards like let Just x | x 0 = e in x The x 0 is understood as an assertion here, documenting an invariant. However, Haskell reads this as let Just x = case () of { () |

Re: [Haskell-cafe] GHC bug? Let with guards loops

The definition Just x | x 0 = Just 1 is recursive. It conditionally defines Just x as Just 1 when x 0 (and as bottom otherwise). So it must know the result before it can test the guard, but it cannot know the result until the guard is tested. Consider an augmented definition: Just x |

Re: [Haskell-cafe] GHC bug? Let with guards loops

it does not make sense to consider variables of g bound by p. Maybe you can cook up some counterexample. I think the pattern variables of p should not be in scope in g, and shadowing free variables of g by pattern variables of p should be forbidden. Cheers, Andreas On 09.07.2013 17:05, Dan

Re: [Haskell-cafe] Int is broken [Was: Different answers on different machines]

There is a package that implements an Int that throws an exception on overflow: http://hackage.haskell.org/package/safeint Since Int's existence is pretty much all about trading for performance, I wouldn't recommend holding your breath on the above becoming the default. If you want things

Re: [Haskell-cafe] Stream fusion and span/break/group/init/tails

On Mon, Apr 29, 2013 at 10:05 AM, Duncan Coutts duncan.cou...@googlemail.com wrote: On Thu, 2013-04-25 at 00:52 +0200, Gábor Lehel wrote: On Wed, Apr 24, 2013 at 7:56 PM, Bryan O'Sullivan b...@serpentine.com wrote: On Wed, Apr 24, 2013 at 10:47 AM, Duncan Coutts

Re: [Haskell-cafe] Why were datatype contexts removed instead of fixing them?

It is not completely backwards compatible, because (for instance) the declaration: newtype C a = Foo a = Foo a was allowed, but: newtype Foo a where Foo :: C a = a - Foo a is an illegal definition. It can only be translated to a non-newtype data declaration, which changes the

Re: [Haskell-cafe] Why were datatype contexts removed instead of fixing them?

in general, though. I haven't missed them, at least. -- Dan On Thu, Apr 25, 2013 at 3:19 PM, Gábor Lehel illiss...@gmail.com wrote: Good point, again. Is that the only problem with it? On Thu, Apr 25, 2013 at 5:57 PM, Dan Doel dan.d...@gmail.com wrote: It is not completely backwards compatible

Re: [Haskell-cafe] Stream fusion and span/break/group/init/tails

Presumably concat also has to use skip, for the same reason as filter. Otherwise it has to recursively process the outer stream until it gets to a non-empty inner stream, which breaks the rule that only the final consumer is recursive. concat [[1,2,3],[4,5],[],[6,7]] probably looks something

Re: Why is GHC so much worse than JHC when computing the Ackermann function?

There's something strange going on in this example. For instance, setting (-M) heap limits as low as 40K seems to have no effect, even though the program easily uses more than 8G. Except, interrupting the program in such a case does seem to give a message about heap limits being exceeded (it won't

Re: [Haskell-cafe] Need some advice around lazy IO

Do note that deepSeq alone won't (I think) change anything in your current code. bug will deepSeq the file contents. And the cons will seq bug. But nothing is evaluating the cons. And further, the cons isn't seqing the tail, so none of that will collapse, either. So the file descriptors will still

Re: [Haskell-cafe] Need some advice around lazy IO

One thing that typically isn't mentioned in these situations is that you can add more laziness. I'm unsure if it would work from just your snippet, but it might. The core problem is that something like: mapM readFile names will open all the files at once. Applying any processing to the file

Re: [Haskell-cafe] Haskell + RankNTypes + (forall p. p Char - p Bool) sound?

Just because you can't use the 'magic primitive' in question to produce an element of the empty type doesn't mean the system is sound (nor does type soundness have anything to do with proving 'false'). The question is what the primitive is supposed to do. If it's supposed to work as a witness of

Re: [Haskell-cafe] Haskell syntax/indentation for vim

I hadn't seen this before, but I tried it out, and the parts I'm interested in are nice. The indenting is less flaky than what I was using before (comments had issues). If you're rewriting things, though, it'd be nice to be able to customize indentation a little more. For instance, I like laying

Re: [Haskell-cafe] Haskell syntax/indentation for vim

, but probably works for almost all cases. Are there any others? On Mon, Mar 04, 2013 at 12:20:12PM -0500, Dan Doel wrote: I hadn't seen this before, but I tried it out, and the parts I'm interested in are nice. The indenting is less flaky than what I was using before (comments had issues

Re: [Haskell-cafe] Inference for RankNTypes

Your example doesn't work for the same reason the following doesn't work: id runST (some st code) It requires the inferencer to instantiate certain variables of id's type to polymorphic types based on runST (or flip's based on one), and then use that information to check some st code (id in

Re: [Haskell-cafe] Inference for RankNTypes

On Wed, Jan 2, 2013 at 11:20 AM, Dan Doel dan.d...@gmail.com wrote: Note that even left-to-right behavior covers all cases, as you might have: f x y such that y requires x to be checked polymorphically in the same way. There are algorithms that can get this right in general, but it's

Re: [Haskell-cafe] Inference for RankNTypes

. If that's still too vague, you'll have to refer to the paper. -- Dan * http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/jfp-outsidein.pdf On Wed, Jan 2, 2013 at 11:47 AM, Francesco Mazzoli f...@mazzo.li wrote: At Wed, 2 Jan 2013 11:20:46 -0500, Dan Doel wrote

Re: Status of Haskell'?

This is a significant problem for even some of the more ubiquitous extensions. For instance, there are multiple compilers that implement RankNTypes, but I would not be surprised at all if programs using that extension were not portable across implementations (they're not really even portable

Re: Status of Haskell'?

MPTCs alone that would be a problem, though. On Sun, Dec 2, 2012 at 2:56 PM, Gábor Lehel illiss...@gmail.com wrote: On Sun, Dec 2, 2012 at 7:06 PM, Dan Doel dan.d...@gmail.com wrote: This is a significant problem for even some of the more ubiquitous extensions. For instance, there are multiple

Re: [Haskell-cafe] Why Kleisli composition is not in the Monad signature?

Lists! The finite kind. This could mean Seq for instance. On Nov 30, 2012 9:53 AM, Brent Yorgey byor...@seas.upenn.edu wrote: On Fri, Nov 30, 2012 at 02:33:54AM +0100, Ben Franksen wrote: Brent Yorgey wrote: On Thu, Nov 29, 2012 at 03:52:58AM +0100, Ben Franksen wrote: Tony Morris

Re: [Haskell-cafe] Why Kleisli composition is not in the Monad signature?

On Tue, Oct 16, 2012 at 10:37 AM, AUGER Cédric sedri...@gmail.com wrote: join IS the most important from the categorical point of view. In a way it is natural to define 'bind' from 'join', but in Haskell, it is not always possible (see the Monad/Functor problem). As I said, from the

Re: [Haskell-cafe] Why Kleisli composition is not in the Monad signature?

On Mon, Oct 15, 2012 at 10:05 PM, damodar kulkarni kdamodar2...@gmail.com wrote: @Jake In my opinion, this is not as nice as the do-notation version, but at least it's compositional: That's an important point you have made, as Haskellers value code composition so much. If code

Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists

On Wed, Sep 26, 2012 at 12:41 AM, o...@okmij.org wrote: First of all, the Boehm-Berarducci encoding is inefficient only when doing an operation that is not easily representable as a fold. Quite many problems can be efficiently tackled by a fold. Indeed. Some operations are even more efficient

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

On Sun, Sep 16, 2012 at 11:49 AM, Simon Peyton-Jones simo...@microsoft.com wrote: I don't really want to eagerly eta-expand every type variable, because (a) we'll bloat the constraints and (b) we might get silly error messages. For (b) consider the insoluble constraint [W] a~b where a

Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists

On Wed, Sep 19, 2012 at 8:36 PM, wren ng thornton w...@freegeek.org wrote: P.S. It is actually possible to write zip function using Boehm-Berarducci encoding: http://okmij.org/ftp/ftp/Algorithms.html#zip-folds Of course it is; I just never got around to doing it :) If you do, you

Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists

This paper: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.957 Induction is Not Derivable in Second Order Dependent Type Theory, shows, well, that you can't encode naturals with a strong induction principle in said theory. At all, no matter what tricks you try. However, A Logic

Re: [Haskell-cafe] Church vs Boehm-Berarducci encoding of Lists

be used to prove statements _about_ the encodings that imply the induction principle. On Tue, Sep 18, 2012 at 4:09 PM, Dan Doel dan.d...@gmail.com wrote: This paper: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.957 Induction is Not Derivable in Second Order Dependent Type

[Haskell-cafe] Fwd: How Type inference work in presence of Functional Dependencies

Copying the mailing list, because I forgot. On Thu, Sep 13, 2012 at 5:18 AM, satvik chauhan mystic.sat...@gmail.com wrote: Consider the code below : {-# LANGUAGE MultiParamTypeClasses,FlexibleInstances,FunctionalDependencies,UndecidableInstances,FlexibleContexts #-} class Foo a c | a - c

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

On Fri, Aug 31, 2012 at 9:06 AM, Edward Kmett ekm...@gmail.com wrote: I know Agda has to jump through some hoops to make the refinement work on pairs when they do eta expansion. I wonder if this could be made less painful. To flesh this out slightly, there are two options for defining pairs in

Re: New INLINE pragma syntax idea, and some questions

On Aug 3, 2012 11:13 PM, Brandon Simmons brandon.m.simm...@gmail.com wrote: In particular I don't fully understand why these sorts of contortions... http://hackage.haskell.org/packages/archive/base/latest/doc/html/src/GHC-List.html#foldl ...are required. It seems like a programmer has to

Re: Call to arms: lambda-case is stuck and needs your help

If we're voting I think \of is all right, and multi-argument case could be handy, which rules out using 'case of' for lambda case, because it's the syntax for a 0-argument case: case of | guard1 - ... | guard2 - ... Then multi-argument lambda case could use the comma syntax

Re: [Haskell-cafe] I Need a Better Functional Language!

On Thu, Apr 5, 2012 at 10:14 AM, Grigory Sarnitskiy sargrig...@ya.ru wrote: First, what are 'functions' we are interested at? It can't be the usual set-theoretic definition, since it is not constructive. The constructive definition should imply functions that can be constructed, computed.

Re: [Haskell-cafe] Monad laws in presence of bottoms

On Tue, Feb 21, 2012 at 10:44 AM, wren ng thornton w...@freegeek.org wrote: That's a similar sort of issue, just about whether undefined == (undefined,undefined) or not. If the equality holds then tuples would be domain products[1], but domain products do not form domains! ... [1] Also a

Re: [Haskell-cafe] Monad laws in presence of bottoms

On Wed, Feb 22, 2012 at 1:40 AM, wren ng thornton w...@freegeek.org wrote: It's a category-theoretic product, but not for the category of domains. Let Set be the category of sets and set-theoretic functions. And let pDCPO be the category of (pointed) domains and their homomorphisms. The

Re: Holes in GHC

On Thu, Jan 26, 2012 at 12:45 PM, Thijs Alkemade thijsalkem...@gmail.com wrote: Let me try to describe the goal better. The intended users are people new to Haskell or people working with existing code they are not familiar with. Also me. I want this feature. It pretty much single handedly

Re: Holes in GHC

On Thu, Jan 26, 2012 at 2:36 PM, Simon Peyton-Jones simo...@microsoft.com wrote: |   Let me try to describe the goal better. The intended users are people |   new to Haskell or people working with existing code they are not |   familiar with. | |  Also me. I want this feature. My question

Re: [Haskell-cafe] Not an isomorphism, but what to call it?

A is a retract of B. http://nlab.mathforge.org/nlab/show/retract g is the section, f is the rectraction. You seem to have it already. The definition needn't be biased toward one of the functions. On Thu, Jan 19, 2012 at 4:24 PM, Sean Leather leat...@cs.uu.nl wrote: I have two types A and

Re: [Haskell-cafe] Why were unfailable patterns removed and fail added to Monad?

On Thu, Jan 19, 2012 at 10:43 PM, Gregory Crosswhite gcrosswh...@gmail.com wrote: first, that the notion of unfailable was not removed from the language so much as not added in the first place No, this is not correct. Unfailable patterns were specified in Haskell 1.4 (or, they were called

Re: [Haskell-cafe] Why were unfailable patterns removed and fail added to Monad?

On Thu, Jan 19, 2012 at 11:11 PM, Dan Doel dan.d...@gmail.com wrote: No, this is not correct. Unfailable patterns were specified in Haskell 1.4 (or, they were called failure-free there; they likely existed earlier, too, but I'll leave the research to people who are interested). They were new

Re: Unit unboxed tuples

On Wed, Jan 11, 2012 at 8:41 AM, Simon Marlow marlo...@gmail.com wrote: On 10/01/2012 16:18, Dan Doel wrote: Copying the list, sorry. I have a lot of trouble replying correctly with gmail's interface for some reason. :) On Tue, Jan 10, 2012 at 11:14 AM, Dan Doeldan.d...@gmail.com  wrote

Re: Unit unboxed tuples

Copying the list, sorry. I have a lot of trouble replying correctly with gmail's interface for some reason. :) On Tue, Jan 10, 2012 at 11:14 AM, Dan Doel dan.d...@gmail.com wrote: On Tue, Jan 10, 2012 at 5:01 AM, Simon Marlow marlo...@gmail.com wrote: On 09/01/2012 04:46, wren ng thornton wrote

Re: [Haskell-cafe] On the purity of Haskell

On Sun, Jan 1, 2012 at 3:26 PM, Ketil Malde ke...@malde.org wrote: Chris Smith cdsm...@gmail.com writes: I wonder: can writing to memory be called a “computational effect”? If yes, then every computation is impure. I wonder if not the important bit is that pure computations are unaffected by

Re: [Haskell-cafe] strict, lazy, non-strict, eager

On Sat, Dec 24, 2011 at 2:31 AM, Albert Y. C. Lai tre...@vex.net wrote: 1. a function f is strict if  f ⊥ = ⊥ 2. ⊥ represents any computation which does not terminate, i.e. an exception or an infinite loop 3. strict describes the denotational semantics All three of these statements are true.

Re: [Haskell-cafe] strict, lazy, non-strict, eager

On Sun, Dec 25, 2011 at 12:14 AM, Eugene Kirpichov ekirpic...@gmail.com wrote: On Sat, Dec 24, 2011 at 10:49 PM, Dan Doel dan.d...@gmail.com wrote: I think it's good to be clear on all these specifics, and people could do with a better recognition of the difference between (non-)strict

Re: [Haskell-cafe] If you'd design a Haskell-like language, what would you do different?

On Thu, Dec 22, 2011 at 4:19 AM, Heinrich Apfelmus apfel...@quantentunnel.de wrote: Alexander Solla wrote: And denotational semantics is not just nice. It is useful. It's the best way to understand why the program we just wrote doesn't terminate. Denotational semantics is unrealistic.  It

Re: [Haskell-cafe] More liberal than liberal type synonyms

On Wed, Dec 7, 2011 at 5:48 AM, Dmitry Kulagin dmitry.kula...@gmail.com wrote: I am still pretty new in Haskell, but this problem annoys me already. If I define certain monad as a type synonym:    type StateA a = StateT SomeState SomeMonad a Then I can't declare new monad based on the

More liberal than liberal type synonyms

Greetings, In the process of working on a Haskell-alike language recently, Ed Kmett and I realized that we had (without really thinking about it) implemented type synonyms that are a bit more liberal than GHC's. With LiberalTypeSynonyms enabled, GHC allows: type Foo a b = b - a type Bar

[Haskell-cafe] More liberal than liberal type synonyms

Greetings, In the process of working on a Haskell-alike language recently, Ed Kmett and I realized that we had (without really thinking about it) implemented type synonyms that are a bit more liberal than GHC's. With LiberalTypeSynonyms enabled, GHC allows: type Foo a b = b - a type Bar

Re: Evaluating type expressions in GHCi

type family Bar a :: * type instance Bar () = String data Foo a = Bar a | Baz a a ghci Bar () What happens? There is a lot of ambiguity between term and type levels in Haskell. (,); []; etc. It's only the overall structure of the language that disambiguates them; you can't necessarily tell

Re: [Haskell-cafe] Smarter do notation

On Sun, Sep 4, 2011 at 12:24 AM, Ivan Lazar Miljenovic ivan.miljeno...@gmail.com wrote: On 4 September 2011 12:34, Daniel Peebles pumpkin...@gmail.com wrote: Hi all, For example, if I write in a do block: x - action1 y - action2 z - action3 return (f x y z) that doesn't require any of the

Re: Type families difference between 7.0.4 and 7.2.1

Classes are not always exported from a module. Only instances are. It is even possible to export methods of a class that isn't itself exported, making it impossible to write the types for them explicitly (GHC will infer qualified types that you can't legally write given the imports). I don't

[Haskell] ANNOUNCE: vector-algorithms 0.5.2

Greetings, Following some work at hac-phi, I've finally put together a new release of vector-algorithms. It should now be available via hackage, or you can pull from code.haskell.org if you prefer: hackage: http://hackage.haskell.org/package/vector-algorithms/ latest: darcs get

[Haskell-cafe] ANNOUNCE: vector-algorithms 0.5.2

Greetings, Following some work at hac-phi, I've finally put together a new release of vector-algorithms. It should now be available via hackage, or you can pull from code.haskell.org if you prefer: hackage: http://hackage.haskell.org/package/vector-algorithms/ latest: darcs get

Re: Superclass Cycle via Associated Type

2011/7/22 Gábor Lehel illiss...@gmail.com: Yeah, this is pretty much what I ended up doing. As I said, I don't think I lose anything in expressiveness by going the MPTC route, I just think the two separate but linked classes way reads better. So it's just a would be nice thing. Do recursive

Re: [Haskell-cafe] Simple GADTs, type families and type classes combination with type error.

On Fri, Jul 22, 2011 at 11:12 AM, Serguey Zefirov sergu...@gmail.com wrote: - {-# LANGUAGE GADTs, TypeFamilies #-} class CPU cpu where        type CPUFunc cpu data Expr cpu

Re: [Haskell-cafe] Simple GADTs, type families and type classes combination with type error.

On Fri, Jul 22, 2011 at 4:11 PM, Serguey Zefirov sergu...@gmail.com wrote: But cpu variable is the same in all places. If we don't dive into CPUFunc reduction (to Int or whatever) we can safely match funcVars argument and unify cpu. This is the case when we write generic functions over type

Re: Superclass Cycle via Associated Type

This isn't a GHC limitation. The report specifies that the class hierarchy must be a DAG. So C cannot require itself as a prerequisite, even if it's on a 'different' type. Practically, in the implementation strategy that GHC (and doubtless other compilers) use, the declaration: class C (A x)

Re: TypeFamilies vs. FunctionalDependencies type-level recursion

On Wed, Jun 15, 2011 at 3:25 AM, Simon Peyton-Jones simo...@microsoft.com wrote: Wait.  What about        instance C [a] [b] ?  Should that be accepted?  The Coverage Condition says no, and indeed it is rejected. But if you add -XUndecidableInstances it is accepted. This 'clearly' violates

Re: TypeFamilies vs. FunctionalDependencies type-level recursion

On Tue, Jun 14, 2011 at 11:27 AM, Andrea Vezzosi sanzhi...@gmail.com wrote:    class C a b | a - b    instance C a R    instance C T U Are you sure that worked before? 80% The following still does anyhow:    data R    data T    data U    class C a b | a - b    instance TypeCast R b =

Re: TypeFamilies vs. FunctionalDependencies type-level recursion

Sorry about the double send, David. I forgot to switch to reply-all in the gmail interface. On Tue, Jun 14, 2011 at 11:49 AM, dm-list-haskell-pr...@scs.stanford.edu wrote: You absolutely still can use FunctionalDependencies to determine type equality in GHC 7.  For example, I just verified the

Re: TypeFamilies vs. FunctionalDependencies type-level recursion

On Tue, Jun 14, 2011 at 1:19 PM, dm-list-haskell-pr...@scs.stanford.edu wrote: No, these are not equivalent.  The first one TypeEq a b c is just declaring an instance that works forall c.  The second is declaring multiple instances, which, if there were class methods, could have different

Re: TypeFamilies vs. FunctionalDependencies type-level recursion

On Sun, May 29, 2011 at 6:45 PM, Ben Millwood hask...@benmachine.co.uk wrote: It would seem very strange to me if haskell-prime made the choice of fundeps/type families based on the behaviour with OverlappingInstances. I'm under the impression that Overlapping is generally considered one of

Re: [Haskell-cafe] Is fusion overrated?

On Wed, May 18, 2011 at 2:04 AM, Ryan Ingram ryani.s...@gmail.com wrote: Yes, the goal isn't so much to improve complexity (both are O(1)) but to reduce the constant factor on that O(1). In an inner loop like that, allocator/gc calls by far dominate the cost of the program.  If you can remove

Re: [Haskell-cafe] Robert Harper on monads and laziness

On Tue, May 3, 2011 at 2:26 AM, Dominique Devriese dominique.devri...@cs.kuleuven.be wrote: What I find interesting is that he considers (non-)termination an effect, which Haskell does not manage to control like it does other types of effects. Dependently typed purely functional languages like

Re: [Haskell-cafe] Python is lazier than Haskell

(Sorry if you get this twice, Ertugrul; and if I reply to top. I'm stuck with the gmail interface and I'm not used to it.) On Thu, Apr 28, 2011 at 11:27 AM, Ertugrul Soeylemez e...@ertes.de wrote: I don't see any problem with this.  Although I usually have a bottom-up approach, so I don't do

Re: Broken ghc-7.0.3/vector combination?

On Wed, Apr 20, 2011 at 3:01 PM, Daniel Fischer daniel.is.fisc...@googlemail.com wrote: I'm sure it's not criterion, because after I've found that NaNs were introduced to the resamples vectors during sorting (check the entire vectors for NaNs before and aftersorting, tracing the count; before:

Re: [Haskell-cafe] Higher-kinded Quantification

On Monday 11 April 2011 8:31:54 PM Leon Smith wrote: I have a type constructor (Iterator i o m a) of kind (* - * - (* - *) - *), which is a monad transformer, and I'd like to use the type system to express the fact that some computations must be pure, by writing the impredicative type

Re: [Haskell-cafe] Higher-kinded Quantification

On Tuesday 12 April 2011 11:27:31 AM Leon Smith wrote: I think impredicative polymorphism is actually needed here; if I write ... Then I get a type error ... I'm not going to worry about the type error, because that wasn't what I had in mind for the types. The type for loop I had in mind

Re: [Haskell-cafe] [Agda] Defining subtraction for naturals

On Thursday 17 March 2011 6:41:33 PM wren ng thornton wrote: How about pragmatically efficacious? Well... (3) Use type hackery to disallow performing subtraction when the result would drop below zero, e.g. by requiring a proof that the left argument is not less than the right. As far as

Re: [Haskell-cafe] linear and dependent types

On Saturday 19 February 2011 1:11:23 AM Vasili I. Galchin wrote: BTW I was thinking of http://www.ats.org when I asked this question. Technically speaking, if one considers ATS to be dependently typed, then one might as well also consider GHC to be dependently typed (with the right extensions

Re: Injective type families?

On Monday 14 February 2011 5:51:55 PM Daniel Peebles wrote: I think what you want is closed type families, as do I and many others :) Unfortunately we don't have those. Closed type families wouldn't necessarily be injective, either. What he wants is the facility to prove (or assert) to the

Re: [Haskell-cafe] ($) not as transparent as it seems

On Thursday 03 February 2011 5:12:54 PM Tim Chevalier wrote: On Thu, Feb 3, 2011 at 2:03 PM, Luke Palmer lrpal...@gmail.com wrote: This is probably a result of strictness analysis. error is technically strict, so it is reasonable to optimize to: let e = error foo in e `seq` error e

Re: In opposition of Functor as super-class of Monad

On Tuesday 04 January 2011 5:24:21 am o...@okmij.org wrote: Method A: just define bind as usual instance (Functor (Iteratee el m),Monad m) = Monad (Iteratee el m) where return = IE_done IE_done a = f = f a IE_cont e k = f = IE_cont e (\s - k s = docase)

Re: [Haskell-cafe] What's the motivation for η rules?

On Monday 03 January 2011 9:23:17 pm David Sankel wrote: The following is a dependent type example where equality of open terms comes up. z : (x : A) → B z = ... w : (y : A) → C w = z Here the compiler needs to show that the type B, with x free, is equivalent to C, with y free. This

Re: [Haskell-cafe] Proof in Haskell

On Thursday 23 December 2010 12:52:07 pm Daniel Peebles wrote: Fair enough :) that'll teach me to hypothesize something without thinking about it! I guess I could amend my coinductive proof: http://hpaste.org/paste/42516/mirrormirror_with_bottom#p42517 does that cover bottom-ness

Re: [Haskell-cafe] Categorical description of systems with dependent types

On Thursday 02 December 2010 10:13:32 am Petr Pudlak wrote: Hi, recently, I was studying how cartesian closed categories can be used to describe typed functional languages. Types are objects and morphisms are functions from one type to another. Since I'm also interested in systems with

Re: [Haskell-cafe] Categorical description of systems with dependent types

On Thursday 02 December 2010 7:54:18 pm Larry Evans wrote: [snip] *Maybe* the computer science people are trying to minimize the concepts. In this case, the one concept common to both the sum and product ( in the math peoples viewpoint) is there's a function: field2type: field_name -

Re: [Haskell-cafe] Serialization of (a - b) and IO a

On Thursday 11 November 2010 9:23:13 pm Luke Palmer wrote: Admittedly, the class of reasoning I usually use in my Haskell programs, and the one that you talked about using earlier this message, is essentially seq doesn't exist. However, I prefer to use this class of reasoning because I would

Re: [Haskell-cafe] Serialization of (a - b) and IO a

It took me a bit to decide whether this was an adequate counter to my objection, but ultimately, I don't think it is. I'll try to explain as well as possible. On Friday 12 November 2010 1:40:10 pm rocon...@theorem.ca wrote: As you are well aware in Coq, and in Agda we don't have an

Re: [Haskell-cafe] Serialization of (a - b) and IO a

On Thursday 11 November 2010 4:25:46 am Thomas Davie wrote: I don't think I agree, I didn't see a rule f == g = serialise f == serialise g anywhere. That equal things can be substituted for one another is one of the fundamental ideas of equality (the other is that anything is equal to itself).

  1   2   3   4   >