[Haskell] Type Lambdas in Gofer
The code in "Bananas in Space: Extending Fold and Unfold to Exponential Types" http://citeseer.ist.psu.edu/293490.html mirror: http://www.cs.nott.ac.uk/~gmh/bananas.pdf uses Gofer, and has examples such as data Rec f = In (f (Rec f)) type P f a = f (Rec f, a) mapP :: Functor f => (a -> b) -> P f a -> P f b mapP g = fmap (\(x,a) -> (x, g a)) instance Functor f => Functor (P f) where fmap = mapP Why did Gofer have this power while Haskell does not? Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: Even higher-order abstract syntax: typeclasses vs GADT
On 1/22/07, Benjamin Franksen <[EMAIL PROTECTED]> wrote: From my very limited understanding of these issues I would say it is not possible, neither with type-classes nor with G[AR]DTs because it would mean the return type of the function 'typecheck' would have to vary depending on the input data, hence you'd need a genuinely dependent type system for such a feat. GADTs are darn near dependent types. Tim Sheard, James Hook, and Nathan Linger caim that extensible kinds complete the equation in "GADTs + Extensible Kinds = Dependent Programming" http://web.cecs.pdx.edu/~sheard/papers/GADT+ExtKinds.ps Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
Re: [Haskell] Re: ANN: Haskell98 termination analyzer (AProVE)
On 9/11/06, Neil Mitchell <[EMAIL PROTECTED]> wrote: Can you give any examples of terminating Haskell programs that a human can analyse (perhaps with a bit of thought), but that your system can't? (I couldn't find any in your paper) Euclid's algorithm is mentioned on the web page, if I remember correctly. Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: kernel 2.6.11 and readline.so
Irina Kaliman wrote: # rpm -ivh ghc-6.4-1.i386.rpm error: Failed dependencies: libreadline.so.4 is needed by ghc-6.4-1.i386 Go to rpmfind.net Type libreadline.so.4 Find the text "Fedora Core 4" Install the compat-readline RPM Fedora has compat projects for other old libraries as well. Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Type of y f = f . f
Jon Fairbairn wrote: If you allow quantification over higher kinds, you can do something like this: d f = f . f d:: âa::*, b::*â*.(b a â a) â b (b a)â a What's the problem with d :: (forall c . b c -> c) -> b (b a) -> a d f = f . f to which ghci gives the type d :: forall a b. (forall c. b c -> c) -> b (b a) -> a It's too restrictive: it requires that the argument to d be polymorphic, so if f:: [Int]->[Int], d f won't typecheck. Oh, that's bad. It also requires that the type of f have an application on the lhs, so f :: Int->Int won't allow d f to typecheck either. This part I don't understand - isn't b anything in *->*? Can't b be the identity functor? Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Type of y f = f . f
Jon Fairbairn wrote: If you allow quantification over higher kinds, you can do something like this: d f = f . f d:: âa::*, b::*â*.(b a â a) â b (b a)â a What's the problem with d :: (forall c . b c -> c) -> b (b a) -> a d f = f . f to which ghci gives the type d :: forall a b. (forall c. b c -> c) -> b (b a) -> a Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Type of y f = f . f
Is there a type we can give to y f = f . f y id y head y fst are all typeable? Jim Apple ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Why is getArgs in the IO monad?
I still think I'm missing your point, but let me take a stab at it. Conal Elliott wrote: I'm suggesting you might better understand the why of Haskell if you think denotationally (here about the meaning of the [String] type), rather than operationally. The meaning of a type seems to be about what happens operationally. ":: [String]" is an operational guarantee, so if we let "getArgs :: [String]" that is a promise that there is some list of Strings at runtime. > I'm guessing that none of those 2^32+1 values is what you'd mean by "length getArgs". Well, I suppose I mean something like an existential type: there is some Int that is length getArgs. Even if this is denotationally different from a value like zero :: Int, I think it is also different from getLine :: IO String. It seems to mean something between these. I suppose my intuition is that it is closer to :: Int Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Why is getArgs in the IO monad?
Tomasz Zielonka wrote: I like to think that pure functions don't change between executions. I'd like to think they wouldn't change within executions. Is there a pure haskell way to check the value of a function between exections? Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Why is getArgs in the IO monad?
Abraham Egnor wrote: It's not a constant; see, for example, System.Environment.withArgs That seems unnecessarily hack-ish. When would one use it when taking a [String] parameter would be inferior? Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Why is getArgs in the IO monad?
Conal Elliott wrote: If getArgs had type [String], then its denotation must be a (lazy) list of (lazy) sequences of characters (extended by bottom). For instance, the expression (words "hello world") denotes the list ["hello","world"]. What list would "getArgs" denote? I don't think I understand your (rhetorical) question. It seems that, looking out at the world from main, the args passed to main and the compilation happen at the same time (before, long long ago). What motivation would we have for treating them differently? Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Why is getArgs in the IO monad?
See subject. It seems that it would be constant through execution, and so could be just [String]. Jim ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
