Re: [Haskell-cafe] Rigid skolem type variable escaping scope
On Aug 23, 2012, at 10:32 PM, wren ng thornton wrote: Now, be careful of something here. The reason this fails is because we're compiling Haskell to System Fc, which is a Church-style lambda calculus (i.e., it explicitly incorporates types into the term language). It is this fact of being Church-style which forces us to instantiate ifn before we can do case analysis on it. If, instead, we were compiling Haskell down to a Curry-style lambda calculus (i.e., pure lambda terms, with types as mere external annotations) then everything would work fine. In the Curry-style world we wouldn't need to instantiate ifn at a specific type before doing case analysis, so we don't have the problem of magicking up a type. And, by parametricity, the function fn can't do anything particular based on the type of its argument, so we don't have the problem of instantiating too early[1]. Okay, I think that's what I was looking for, and that makes perfect sense. Thank you! Of course, (strictly) Curry-style lambda calculi are undecidable after rank-2 polymorphism, and the decidability at rank-2 is pretty wonky. Hence the reason for preferring to compile down to a Church-style lambda calculus. There may be some intermediate style which admits your code and also admits the annotations needed for inference/checking, but I don't know that anyone's explored such a thing. Curry-style calculi tend to be understudied since they go undecidable much more quickly. Gotcha. So if I'm understanding correctly, it sounds like the answer to one of my earlier questions is (very) roughly, Yes, the original version of bar would be typesafe at runtime if the typechecker were magically able to allow it, but GHC doesn't allow it because trying to do so would get us into undecidability nastiness and isn't worth it. Which is sort of what I expected, but I couldn't figure out why; now I know. I think now I will go refresh myself on System F (it's been a while) and read up on System Fc (which I wasn't previously aware of). (-: Cheers, -Matt ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Rigid skolem type variable escaping scope
While working on a project I have come across a new-to-me corner case of the
type system that I don't think I understand, and I am hoping that someone here
can enlighten me.
Here's a minimal setup. Let's say I have some existing code like this:
{-# LANGUAGE Rank2Types #-}
class FooClass a where ...
foo :: (forall a. (FooClass a) = a - Int) - Bool
foo fn = ...
Now I want to make a type alias for these (a - Int) functions, and give myself
a new way to call foo. I could do this:
type IntFn a = a - Int
bar :: (forall a. (FooClass a) = IntFn a) - Bool
bar fn = foo fn
This compiles just fine, as I would expect. But now let's say I want to change
it to make IntFn a newtype:
newtype IntFn a = IntFn (a - Int)
bar :: (forall a. (FooClass a) = IntFn a) - Bool
bar (IntFn fn) = foo fn
I had expected this to compile too. But instead, I get an error like this one
(using GHC 7.4.1):
Couldn't match type `a0' with `a'
because type variable `a' would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context: FooClass a = a - Int
The following variables have types that mention a0
fn :: a0 - Int (bound at the line number that implements bar)
In the first argument of `foo', namely `fn'
In the expression: foo fn
In an equation for `bar': bar (IntFn fn) = foo fn
I don't think I am grasping why adding the layer of newtype
wrapping/unwrapping, without otherwise changing the types, introduces this
problem. Seems to me like the newtype version would also be type-safe if GHC
allowed it (am I wrong?), and I'm failing to understand why GHC can't allow it.
Is there a simple explanation, or else some reading that someone could point
me to? (-:
Cheers,
-Matt
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rigid skolem type variable escaping scope
On Aug 22, 2012, at 3:02 PM, Lauri Alanko wrote:
Quoting Matthew Steele mdste...@alum.mit.edu:
{-# LANGUAGE Rank2Types #-}
class FooClass a where ...
foo :: (forall a. (FooClass a) = a - Int) - Bool
foo fn = ...
newtype IntFn a = IntFn (a - Int)
bar :: (forall a. (FooClass a) = IntFn a) - Bool
bar (IntFn fn) = foo fn
In case you hadn't yet discovered it, the solution here is to unpack the
IntFn a bit later in a context where the required type argument is known:
bar ifn = foo (case ifn of IntFn fn - fn)
Hope this helps.
Ah ha, thank you! Yes, this solves my problem.
However, I confess that I am still struggling to understand why unpacking
earlier, as I originally tried, is invalid here. The two implementations are:
1) bar ifn = case ifn of IntFn fn - foo fn
2) bar ifn = foo (case ifn of IntFn fn - fn)
Why is (1) invalid while (2) is valid? Is is possible to make (1) valid by
e.g. adding a type signature somewhere, or is there something fundamentally
wrong with it? (I tried a few things that I thought might work, but had no
luck.)
I can't help feeling like maybe I am missing some small but important piece
from my mental model of how rank-2 types work. (-: Maybe there's some paper
somewhere I need to read?
Cheers,
-Matt
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Rigid skolem type variable escaping scope
On Aug 22, 2012, at 4:32 PM, Erik Hesselink wrote:
On Wed, Aug 22, 2012 at 10:13 PM, Matthew Steele mdste...@alum.mit.edu
wrote:
On Aug 22, 2012, at 3:02 PM, Lauri Alanko wrote:
Quoting Matthew Steele mdste...@alum.mit.edu:
{-# LANGUAGE Rank2Types #-}
class FooClass a where ...
foo :: (forall a. (FooClass a) = a - Int) - Bool
foo fn = ...
newtype IntFn a = IntFn (a - Int)
bar :: (forall a. (FooClass a) = IntFn a) - Bool
bar (IntFn fn) = foo fn
In case you hadn't yet discovered it, the solution here is to unpack the
IntFn a bit later in a context where the required type argument is known:
bar ifn = foo (case ifn of IntFn fn - fn)
Hope this helps.
Ah ha, thank you! Yes, this solves my problem.
However, I confess that I am still struggling to understand why unpacking
earlier, as I originally tried, is invalid here. The two implementations
are:
1) bar ifn = case ifn of IntFn fn - foo fn
2) bar ifn = foo (case ifn of IntFn fn - fn)
Why is (1) invalid while (2) is valid? Is is possible to make (1) valid by
e.g. adding a type signature somewhere, or is there something fundamentally
wrong with it? (I tried a few things that I thought might work, but had no
luck.)
I can't help feeling like maybe I am missing some small but important piece
from my mental model of how rank-2 types work. (-: Maybe there's some
paper somewhere I need to read?
Look at it this way: the argument ifn has a type that says that *for
any type a you choose* it is an IntFn. But when you have unpacked it
by pattern matching, it only contains a function (a - Int) for *one
specific type a*. At that point, you've chosen your a.
The function foo wants an argument that works for *any* type a. So
passing it the function from IntFn isn't enough, since that only works
for *one specific a*. So you pass it a case expression that produces a
function for *any a*, by unpacking the IntFn only inside.
Okay, that does make sense, and I can see now why (2) works while (1) doesn't.
So my next question is: why does unpacking the newtype via pattern matching
suddenly limit it to a single monomorphic type? As you said, ifn has the type
something that can be an (IntFn a) for any a you choose. Since an (IntFn a)
is just a newtype around an (a - Int), why, when you unpack ifn into (IntFn
fn), is the type of fn not something that can be an (a - Int) for any a you
choose? Is it possible to add a local type annotation to force fn to remain
polymorphic?
Cheers,
-Matt
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] for = flip map
Doesn't for already exist, in Data.Traversable? Except that for = flip traverse. http://www.haskell.org/hoogle/?hoogle=for Cheers, -Matthew On Wed, Mar 28, 2012 at 3:58 PM, Johannes Waldmann waldm...@imn.htwk-leipzig.de wrote: Good: we have mapM, and we have forM ( = flip mapM ) . Sure this is just a convenience, and indeed forM xs $ \ x - do ... is quite handy, especially if xs is really small, and ... is some larger expression. Bad: we have map, but we are missing: for ( = flip map ) . The function is very convenient, for the same reasons as above. I can't remember how often I typed for = flip map in a source file. I never put this definition in a module either, since the import statement would be longer than the definition. So, I'm all for for . In Data.List? In the Prelude? (Should put it right next to map.) - J.W. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] for = flip map
On Mar 28, 2012, at 4:19 PM, Christopher Done wrote: On 28 March 2012 22:05, Matthew Steele mdste...@alum.mit.edu wrote: Doesn't for already exist, in Data.Traversable? Except that for = flip traverse. Traverse doesn't fit the type of fmap, it demands an extra type constructor: traverse :: (Traversable t,Applicative f) = (a - f b) - t a - f (t b) fmap :: Functor f = (a - b) - f a - f b Note the (a - f b) instead of (a - b). E.g. fmap :: (a - b) - [a] - [b] can't be expressed with traverse, you can only get this far: traverse :: (a - [b]) - [a] - [[b]] Unless I'm missing something. That right; I was simply pointing out that the name 'for' is already taken by an existing base function. Things might be more consistant if 'traverse' and 'for' were instead called 'mapA' and 'forA' (by analogy with 'mapM' and 'forM'). Then one could add 'for = flip map' to base without conflict. But for some reason, that's not the case. Cheers, -Matthew ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Why aren't there anonymous sum types in Haskell?
On Jun 21, 2011, at 4:02 PM, Malcolm Wallace wrote: On 21 Jun 2011, at 20:53, Elliot Stern wrote: A tuple is basically an anonymous product type. It's convenient to not have to spend the time making a named product type, because product types are so obviously useful. Is there any reason why Haskell doesn't have anonymous sum types? If there isn't some theoretical problem, is there any practical reason why they haven't been implemented? The Either type is the nearest Haskell comes to having anonymous sum types. If you are bothered because Either has a name and constructors, it does not take long before you realise that (,) has a name and a constructor too. Yes, Either is to sum types what (,) is to product types. The difference is that there is no anonymous sum type equivalent to (,,) and (,,,) and () and so on, which I think is what the original question is getting at. Indeed, I sometimes wish I could write something like (straw-man syntax): foo :: (Int | Bool | String | Double) - Int foo x = case x of 1stOf4 i - i + 7 2ndOf4 b - if b then 1 else 0 3rdOf4 s - length s 4thOf4 d - floor d bar :: Int bar = foo (2ndOf4 True) and have that work for any size of sum type. But I can't. Cheers, -Matt ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Can it be proven there are no intermediate useful type classes between Applicative Functors Monads?
On Mon, Jun 6, 2011 at 3:39 PM, Casey McCann syntaxgli...@gmail.com wrote: On Mon, Jun 6, 2011 at 12:19 PM, Brent Yorgey byor...@seas.upenn.edu wrote: The idea is that Applicative computations have a fixed structure which is independent of intermediate results; Monad computations correspond to (potentially) infinitely branching trees, since intermediate results (which could be of an infinite-sized type) can be used to compute the next action; but Branching computations correspond to *finitely* branching trees, since future computation can depend on intermediate results, but only one binary choice at a time. Is this truly an intermediate variety of structure, though? Or just different operations on existing structures? With Applicative, there are examples of useful structures that truly can't work as a Monad, the usual example being arbitrary lists with liftA2 (,) giving zip, not the cartesian product. Do you know any examples of both: 1) Something with a viable instance for Branching, but either no Monad instance, or multiple distinct Monad instances compatible with the Branching instance I think Branching is to Monad what ArrowChoice is to ArrowApply. Branching allows the shape of the computation to depend on run-time values (which you can't do with Applicative), but still allows only a finite number of computation paths. By purposely making a functor an instance of Branching but _not_ of Monad, you allow it to have some amount of run-time flexibility while still retaining the ability to statically analyze the effects of a computation in that functor. branchApplicative = liftA3 (\b t f - if b then t else f) This definition doesn't satisfy the laws given for the Branching class; it will execute the effects of both branches regardless of which is chosen. Cheers, -Matt ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Calling a C function that returns a struct by value
From Haskell, I want to call a C function that returns a struct by
value (rather than, say, returning a pointer). For example:
typedef struct { double x; double y; } point_t;
point_t polar(double theta);
I can create a Haskell type Point and make it an instance of Storable
easily enough:
data Point = Point CDouble CDouble
instance Storable Point where -- insert obvious code here
And now I want to do something like this:
foreign import ccall unsafe polar :: CDouble - IO Point
...but that doesn't appear to be legal (at least in GHC 6.12). Is
there any way to import this C function into Haskell _without_ having
any additional wrapper C code? I mean, I suppose I could write
something like:
// C:
void polar_wrapper(double theta, point_t* output) {
*output = polar(theta);
}
-- Haskell:
foreign import ccall unsafe polar_wrapper :: CDouble - Ptr Point -
IO ()
polar :: CDouble - IO Point
polar theta = do -- insert obvious code here
...but that's a lot of extra boilerplate if I have many such functions
to wrap, and it seems like GHC should be able to do that sort of thing
for me. P-:
Cheers,
-Matt
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] naming convention for maybes?
In my own code, I usually use a 'mb' prefix with camelCase, like so: case mbStr of Just str - ... Nothing - ... But I agree that it doesn't always look very nice. I'm curious what others do. On Apr 22, 2011, at 1:14 PM, Evan Laforge wrote: Here's a simple issue that's been with me for a while. As do many people, I use plural variable names for lists, so if a Block as called 'block' then [Block] is 'blocks'. The other pattern that comes up a lot is 'Maybe Block'. When I have to name it, I call it 'maybe_block', e.g. maybe_block - lookup something case maybe_block of Just block - ... However, this maybe_ prefix is rather long and unwieldy. I have considered things like 'm' or 'mb' but they don't suggest Maybe to me. An 'm' prefix or suffix is already implying 'monad'. If '?' were allowed in identifiers I could use it as a suffix. I could just append 'q' and get used to it... lispers did it with 'p' after all. I suppose 'mby' could be ok, but for some reason it just looks ugly to me. 'opt' looks ok, I suppose, but 'optional' doesn't cover the full range of Maybe's usage (i.e. it's strange to call a failed lookup result optional). Does anyone else have a nice convention for this? Hopefully something short but intuitive and nicely reading like the plural convention? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ArrowLoop and streamprocessors
On Mar 30, 2011, at 5:29 PM, Mathijs Kwik wrote: So loop really doesn't seem to help here, but I couldn't find another way either to feed outputs back into the system. What I need is: Either A B ~ Either C B - A ~ C Does such a thing exist? Based on your description, it sounds to me like you want a loop such that if a B is generated at the end, you send it back to the start and execute your arrow a second time. Is that in fact what you intended? However, the docs for ArrowLoop's loop function make it clear that it executes the arrow only once: http://www.haskell.org/ghc/docs/latest/html/libraries/base-4.3.1.0/Control-Arrow.html#v :loop If your arrows are instances of ArrowApply, I believe you could use app to implement the combinator you want. Cheers, -Matt ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] getting last char of String
Sounds like you're looking for `last', which is in the Prelude. http://www.haskell.org/ghc/docs/6.12.2/html/libraries/base-4.2.0.1/Prelude.html#v%3Alast Cheers, -Matt On Dec 31, 2010, at 3:39 PM, Aaron Gray wrote: Is there an easy Haskell function that gets the last Char of a [Char] or String ? Many thanks in advance, Aaron ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Musings on type systems
TAPL is also a great book for getting up to speed on type theory: http://www.cis.upenn.edu/~bcpierce/tapl/ I am no type theorist, and I nonetheless found it very approachable. I've never read TTFP; I will have to check that out. (-: On Nov 19, 2010, at 4:31 PM, Daniel Peebles wrote: There's a lot of interesting material on this stuff if you start poking around :) http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ might be a good introduction. I'd consider typeclasses to be sets of types, as you said, but more generally, a relation of types. In that view, an MPTC is just an n-ary relation over types. Yes, you can get arbitrarily deep on the hierarchy of types and kinds. Agda does this, and even lets you define things that are polymorphic on the universe level. If you do read through TTFP, you might want to follow along with Agda, as it fits quite nicely. On Fri, Nov 19, 2010 at 4:05 PM, Andrew Coppin andrewcop...@btinternet.com wrote: OK, so how do types actually work? Musing on this for a moment, it seems that declaring a variable to have a certain type constrains the possible values that the variable can have. You could say that a type is some sort of set, and that by issuing a type declaration, the compiler statically guarantees that the variable's value will always be an element of this set. Now here's an interesting thought. Haskell has algebraic data types. Algebraic because they are sum types of product types (or, equivilently, product types of sum types). Now I don't actually know what those terms mean, but proceeding by logical inferrence, it seems that Either X Y defines a set that could be described as the union or sum of the types X and Y. So is Either what is meant by a sum type? Similarly, (X, Y) is a set that could be considered the Cartesian product of the sets X and Y. It even has product in the name. So is this a product type? So not only do we have types which denote sets of possible values, but we have operators for constructing new sets from existing ones. (Mostly just applying type constructors to arguments.) Notionally (-) is just another type constructor, so functions aren't fundamentally different to any other types - at least, as far as the type system goes. Now, what about type variables? What do they do? Well now, that seems to be slightly interesting, since a type variable holds an entire type (whereas normal program variables just hold a single value), and each occurrance of the same variable is statically guaranteed to hold the same thing at all times. It's sort of like how every instance of a normal program variable holds the same value, except that you don't explicitly say what that value is; the compiler infers it. So what about classes? Well, restricting ourselves to single- parameter classes, it seems to me that a class is like a *set of types*. Now, interestingly, an enumeration type is a set of values where you explicitly list all possible values. But once defined, it is impossible to add new values to the set. You could say this is a closed set. A type, on the other hand, is an open set of types; you can add new types at any time. I honestly can't think of a useful intuition for MPTCs right now. Now what happens if you add associated types? For example, the canonical class Container c where type Element c :: * We already have type constructor functions such as Maybe with takes a type and constructs a new type. But here we seem to have a general function, Element, which takes some type and returns a new, arbitrary, type. And we define it by a series of equations: instance Container [x] where Element [x] = x instance Container ByteString where Element ByteString = Word8 instance (Ord x) = Container (Set x) where Element (Set x) = x instance Container IntSet where Element IntSet = Int ... Further, the inputs to this function are statically guaranteed to be types from the set (class) Container. So it's /almost/ like a regular value-level function, just with weird definition syntax. Where *the hell* do GADTs fit in here? Well, they're usually used with phantom types, so I guess we need to figure out where phantom types fit in. To the type checker, Foo Int and Foo Bool are two totally seperate types. In the phantom type case, the set of possible values for both types are actually identical. So really we just have two names for the same set. The same thing goes for a type alias (the type keyword). It's not quite the same as a newtype, since then the value expressions do actually change. So it seems that a GADT is an ADT where the elements of the set are assigned to sets of different names, or the elements are partitioned into disjoint sets with different names. Hmm, interesting. At the same type, values have types, and types have kinds. As best as I can tell, kinds exist only to distinguish between /types/ and / type
[Haskell-cafe] Equivalent of withForeignPtr for System.Mem.Weak?
I have an object to which I have added one or more finalizers via
addFinalizer from System.Mem.Weak. I would like to have a function
that allows me to make use of the object within a block of IO code,
and guarantee that the finalizer(s) will not be called during the code
block -- sort of like withForeignPtr, but for arbitrary objects. Does
such a function exist, and if not, how could I write one?
I can imagine writing something like:
\begin{code}
withObject :: a - IO b - IO b
withObject obj action = do
result - action
touchObject obj -- touchObject :: a - IO ()
return result
\end{code}
However, I don't know how I should implement touchObject and be
confident that it won't ever be optimized out. Any suggestions?
Cheers,
-Matt
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
