Re: Why cannot inferred type signatures restrict (potentially) ambiguous type variables?

2013-10-14 Thread Nicolas Frisby
An observation: on GHC 7.6.3, if I remove c2 entirely, then ghci cooperates. *Main :t \x - c (c x) \x - c (c x) :: (C a b, C a1 a) = a1 - b At first blush, I also expected the definition -- no signature, no ascriptions c2 x = c (c x) to type-check. Perhaps GHC adopted a trade-off giving

Re: TypeHoles behaviour

2013-08-27 Thread Nicolas Frisby
I also say +1, but I am concerned about always showing all the bindings. In my experiences over the years, the times when holes seem they would have been most helpful is when the bindings were numerous and had large and complicated types. Dumping all of the bindings in that sort of scenario would

Re: Marking type constructor arguments as nominal (e.g. Set)

2013-08-18 Thread Nicolas Frisby
Is the non-injectivity not an issue here because the type family application gets immediately simplified? On Sun, Aug 18, 2013 at 12:45 PM, Joachim Breitner m...@joachim-breitner.de wrote: Hi, now that roles are in HEAD, I could play around a bit with it. They were introduced to solve the

Re: Marking type constructor arguments as nominal (e.g. Set)

2013-08-18 Thread Nicolas Frisby
than is required to read it. :P On Sun, Aug 18, 2013 at 3:37 PM, Joachim Breitner m...@joachim-breitner.dewrote: Hi, not sure – where would injectivity be needed? Greetings, Joachim Am Sonntag, den 18.08.2013, 15:00 -0500 schrieb Nicolas Frisby: Is the non-injectivity not an issue here

Re: Exposing newtype coercions to Haskell

2013-07-03 Thread Nicolas Frisby
On Wed, Jul 3, 2013 at 5:33 AM, Joachim Breitner m...@joachim-breitner.dewrote: [snip] strange, why did I miss that? But I can’t get [the GlobalRdrEnv lookup] to work, even looking up an element that I took from the GRE itself returns []: let e' = head (head (occEnvElts env))

Re: Exposing newtype coercions to Haskell

2013-07-02 Thread Nicolas Frisby
This is an exciting effort! Just a quick reaction to Simon's comments on CoreM. On Tue, Jul 2, 2013 at 9:11 AM, Simon Peyton-Jones simo...@microsoft.comwrote: To your questions: ** **·**To do these kind of things, CoreM will need more reader stuff. In particular: **o

SpecConstr and GADTs

2012-12-10 Thread Nicolas Frisby
I suspect I've found a situation where, to a first approximation, I'd like SpecConstr to run more than once. I'm specializing on GADT constructors that contain coercions, so the constructor-specialized functions have RHSs with refined types. In my situation, those refined types enable

Re: Generating random type-level naturals

2012-11-16 Thread Nicolas Frisby
When wren's email moved this thread to the top of my inbox, I noticed that I never sent this draft I wrote. It gives some concrete code along the line of Wren's suggestion. - The included code uses a little of this (singleton types) and a little of that (implicit configurations).

Re: Unexpected ambiguity in a seemingly valid Haskell 2010 program

2012-11-09 Thread Nicolas Frisby
My GHC 7.6.1 (on a Mac) compiles this code without any warnings or errors. Do you have some other compilation flags in effect? On Fri, Nov 9, 2012 at 11:09 AM, Roman Cheplyaka r...@ro-che.info wrote: For this module module Test where import System.Random data RPS = Rock |

Re: Using DeepSeq for exception ordering

2012-11-08 Thread Nicolas Frisby
And the important observation is: all of them throw A if interpreted in ghci or compiled without -O, right? On Thu, Nov 8, 2012 at 11:24 AM, Albert Y. C. Lai tre...@vex.net wrote: On 12-11-08 07:12 AM, Simon Hengel wrote: I was just going to say that I can give at least one counterexample

Re: Kind refinement in type families with PolyKinds

2012-10-30 Thread Nicolas Frisby
I share an observation/workaround below. On Tue, Oct 30, 2012 at 8:49 AM, Andres Löh andres.l...@gmail.com wrote: This one looks strange to me: -- Stripping a type from all its arguments type family Strip (t :: *) :: k I'd be tempted to read this as saying that Strip :: forall k. * - k

Re: Proposal: EPHEMERAL pragma

2012-10-25 Thread Nicolas Frisby
The question of whether the warnings should come by default or not is a question of how serious the programmer is when they declare a type as EPHEMERAL. In Pedro's use cases, I would be very serious about it — as Ryan said, performance tends to tank otherwise. ### Proposal Extensions I think a

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

2012-10-11 Thread Nicolas Frisby
On Wed, Sep 19, 2012 at 1:51 PM, Richard Eisenberg e...@cis.upenn.edu wrote: As for recovering kind classes and such once Any is made into a type family: I'm in favor of finding some way to do explicit kind instantiation, making the Any trick obsolete. I'm happy to leave it to others to

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

2012-10-11 Thread Nicolas Frisby
On Thu, Oct 11, 2012 at 10:20 PM, Nicolas Frisby nicolas.fri...@gmail.com wrote: The to my trick key is to use the promotion of this data type. The key to my trick is to use the promotion of this data type. Wow — I have no idea what happened

Re: seemingly inconsistent behavior for kind-indexed type constraints in GHC 7.6

2012-10-08 Thread Nicolas Frisby
On Fri, Oct 5, 2012 at 9:25 PM, Richard Eisenberg e...@cis.upenn.edu wrote: For similar reasons, GHC does not bring the constraints on an instance into the context when an instance matches. So, even if GHC did select the instance you want, it would not bring ('[] ~ ps) into the context. Ah,

Re: seemingly inconsistent behavior for kind-indexed type constraints in GHC 7.6

2012-10-08 Thread Nicolas Frisby
for the noise/HTH in the future. On Mon, Oct 8, 2012 at 1:52 AM, Nicolas Frisby nicolas.fri...@gmail.com wrote: On Fri, Oct 5, 2012 at 9:25 PM, Richard Eisenberg e...@cis.upenn.edu wrote: For similar reasons, GHC does not bring the constraints on an instance into the context when an instance

Re: Constructing TH types

2012-10-07 Thread Nicolas Frisby
The issue you had with applications of the [] type seems to be more insidious than my last email made it out to be. This expression ( $(return $ ConE (mkName [])) :: $(return $ ConT (mkName []) `AppT` ConT ''Char) ) fails with [] is applied to too many arguments. I'm thinking that the []

Re: seemingly inconsistent behavior for kind-indexed type constraints in GHC 7.6

2012-10-06 Thread Nicolas Frisby
in the file, but I'm not sure. Thanks for posting! Richard On Oct 5, 2012, at 5:49 PM, Nicolas Frisby wrote: GHC 7.6 is rejecting some programs that I think ought to be well-typed. Details here https://gist.github.com/3842579 I find this behavior particularly odd because I can get GHC to deduce

Re: seemingly inconsistent behavior for kind-indexed type constraints in GHC 7.6

2012-10-06 Thread Nicolas Frisby
On Sat, Oct 6, 2012 at 12:46 PM, Gábor Lehel illiss...@gmail.com wrote: What do you use NLong for? I.e. where and how are you taking advantage of the knowledge that the list is N long? OK, some context. I'm experimenting with an augmentation of the generic-deriving generic programming approach.

Re: Comments on current TypeHoles implementation

2012-10-04 Thread Nicolas Frisby
tl;wr Variables and holes should have disparate syntax, so that code is easy to locally parse. Simon, your proposal is very crisp from the GHC implementor's perspective, but I think it might be harmful from the user's perspective. My premise is that free variables — which are normally fatal —

Re: Comments on current TypeHoles implementation

2012-10-04 Thread Nicolas Frisby
On Thu, Oct 4, 2012 at 4:28 PM, Roman Cheplyaka r...@ro-che.info wrote: I don't see why it is an issue. You should never encounter holes in the released code. The only source of holes should be stuff that you just wrote. With this proposal not only you get an error for the unbound variable (as

Re: Problem with default signatures

2012-08-23 Thread Nicolas Frisby
I've investigated this behavior a bit, and I have two things worth mentioning. (1) One of the ingredients in this behavior is the non-injectivity of type families. If we make the class parameter f accessible in the signature of emptyAlt, there are no more type errors. For example, if you can

Re: Request for comments on proposal for literate programming using markdown

2012-08-22 Thread Nicolas Frisby
On Wed, Aug 22, 2012 at 10:02 AM, Nicolas Frisby nicolas.fri...@gmail.com wrote: Maybe just try again in a separate thread? Perhaps under a pseudonym! :) Whoa, just realized once again that email is tone-deaf. I meant that 'pseudonym' thing cheekily: just to help differentiate the proposal

Re: faking universal quantification in constraints

2012-04-17 Thread Nicolas Frisby
is kind of irrelevant ... Regarding impredicativity in GHC, we are still unfortunately on the whiteboard ... Hope this helps! d- -Original Message- From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell- users-boun...@haskell.org] On Behalf Of Nicolas Frisby

Re: faking universal quantification in constraints

2012-04-17 Thread Nicolas Frisby
that the corresponding instances was totally polymorphic in the argument. That's bogus reasoning because of ~ (and hence fundeps, as you used). Thanks again. On Tue, Apr 17, 2012 at 2:14 PM, Nicolas Frisby nicolas.fri...@gmail.com wrote: Thanks! I'll analyze what you've done here. One thing that jumps out

Re: faking universal quantification in constraints

2012-04-17 Thread Nicolas Frisby
Great! I'll take a whack at it ;) On Tue, Apr 17, 2012 at 4:07 PM, Edward Kmett ekm...@gmail.com wrote: On Mon, Apr 16, 2012 at 6:57 PM, Nicolas Frisby nicolas.fri...@gmail.com wrote: I'm simulating skolem variables in order to fake universal quantification in constraints via unsafeCoerce

Re: faking universal quantification in constraints

2012-04-17 Thread Nicolas Frisby
is definitely trying to subvert it; so I vote trustworthy. I'm adopting Data.Constraints.Forall for my local experimentation. Thanks for pointing it out. On Tue, Apr 17, 2012 at 4:15 PM, Nicolas Frisby nicolas.fri...@gmail.com wrote: Great! I'll take a whack at it ;) On Tue, Apr 17, 2012 at 4:07

faking universal quantification in constraints

2012-04-16 Thread Nicolas Frisby
I'm simulating skolem variables in order to fake universal quantification in constraints via unsafeCoerce. http://hpaste.org/67121 I'm not familiar with various categories of types from the run-time's perspective, but I'd be surprised if there were NOT a way to use this code to create run-time

Re: How to declare polymorphic instances for higher-kinded types?

2012-03-16 Thread Nicolas Frisby
Here's another alternative. newtype Comp f g a = Comp {unComp :: f (g a)} instance Resolvable e = Resolvable (Maybe `Comp` e) where resolve db = fmap Comp . resolveMaybe db . unComp One disadvantage of this approach is that it requires you to pepper your types with explicit compositions of

packaged up polykinded types can't index type families?

2012-03-13 Thread Nicolas Frisby
I suspect I'm tripping on a gap in the PolyKinds support. I'm trying to package up a type-level generic view. It uses PolyKinds — and DataKinds, but I think it's the PolyKinds that matter. If I compile everything locally in the same build, it works fine. If I isolate the spine view declarations in

Re: ConstraintKinds and default associated empty constraints

2012-01-09 Thread Nicolas Frisby
Just a note: as section 6 of [1] notes, one way (possibly the only?) to satisfy a universally quantified constraint would be a suitably polymorphic instance — i.e. with a type variable in the head. I think this would mitigate the need for whole program analysis at least in some cases, including

Re: Records in Haskell

2012-01-03 Thread Nicolas Frisby
Disclaimer: this use case for type-level string ops is still hypothetical, so these are predictions. Shooting for the moon, I foresee writing a type-level string similarity metric. In my experience, that would involve nested traversals, sliding of sequence windows, etc. In that case, I would very

Re: Records in Haskell

2012-01-02 Thread Nicolas Frisby
I'm interested in type-level strings myself. I'm using an approximation in order to enrich the instant-generics-style reflection of data type declarations with a sensitivity to constructor names. For example, this lets me automatically convert between many the similarly-named constructors of

Superclass Cycle via Associated Type

2011-12-07 Thread Nicolas Frisby
(Sorry I'm so late to this dialogue.) In http://www.haskell.org/pipermail/glasgow-haskell-users/2011-July/020593.html, SPJ asks The superclasses are recursive but   a) They constrain only type variables   b) The variables in the superclass context are all       mentioned in the head.  In