Re: Feedback request: priority queues in containers
Specifically, we use a binomial heap, which offers O(log n) worst-case union O(log n) worst-case extract (this in particular was a key objective of ours) amortized O(1), worst-case O(log n) insertion. (In a persistent context, the amortized performance bound does not necessarily hold.) Why not use Okasaki Brodal's Optimal Purely Functional Priority Queues? They offer worst case: * O(1) union, findMin, and insert * O(lg n) deleteMin http://www.eecs.usma.edu/webs/people/okasaki/jfp96/index.html ftp://ftp.daimi.au.dk/pub/BRICS/Reports/RS/96/37/BRICS-RS-96-37.pdf ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Feedback request: priority queues in containers
I wrote a pretty efficient skew binomial heap implementation -- the first
step of Okasaki's approach -- and found it was already slower than the
optimized binomial heap. I'm not sure whether or not I uploaded that
benchmark, though. I'll do that at some point today, just to keep everyone
happy.
The skew binomial heaps you implemented should only be asymptotically
faster than the usual binomial heaps on one special case: comparing a
binomial heap in a state that would case an \Omega(lg n) time cascade
on insert to the worst-case O(1) insert of binomial heaps.
I think it would also be worth comparing binomial heap merge against
Brodal-Okasaki heap merge.
Finally, if speed is the ultimate goal, I suspect the clever nested
type approach to guaranteeing binomial tree shape slows things down a
bit. For reference, the type in the latest patch is:
data BinomForest rk a = Nil
| Skip !(BinomForest (Succ rk) a)
| Cons {-# UNPACK #-} !(BinomTree rk a)
!(BinomForest (Succ rk) a)
data BinomTree rk a = BinomTree a (rk a)
data Succ rk a = Succ {-# UNPACK #-} !(BinomTree rk a) (rk a)
data Zero a = Zero
I suspect the following might be faster:
data BinomForest2 a = Empty
| NonEmpty a [BinomTree2 a]
data BinomTree2 a = BinomTree2 a [BinomTree2 a]
This eliminates the Skip constructor, which contributes only to the
nested type guarantee.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
[Haskell-cafe] Running classical logic
We can't safely extract a t out of IO t, but we can run an IO t, interact with the environment, and then see the t. Griffin ( http://citeseer.ist.psu.edu/griffin90formulaeastypes.html ) explained that we can do the same thing with (t - r) - r by interacting with the context. That is, he defined a function c :: ((t - r) - r) - t buy interaction with the reduction context of calls to c. I don't expect such a function to be definable in Haskell without some magic, but even with magic, I'm not sure how to write such a function. On #haskell a couple of days ago, we came up with data Empty deriving Typeable toEmpty :: a - Empty toEmpty = unsafeCoerce fromEmpty :: Empty - a fromEmpty = unsafeCoerce type Bot = forall x . x griffinC :: Cont Bot a - IO a griffinC (Cont f) = do key - newUnique catch (evaluate $ f $ \v - throwDyn (hashUnique key,toEmpty v)) (\x - case x of DynException d - case fromDynamic d of Just (u,y) - if u == hashUnique key then return $ fromEmpty y else throwIO x Nothing - throwIO x _ - throwIO x) The Unique is used to keep the later griffinC calls from being cast to the wrong types. The more I look at this, the less I understand it. Any clues? Jim P.S. Thanks to #haskell, and especially roconnor for the fine help ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: Rank-2 polymorphism and pattern matching
On Jan 7, 2008 1:37 AM, Simon Peyton-Jones [EMAIL PROTECTED] wrote: Sadly, it's not true in Haskell, is it? (error urk) : [] also has type (forall a. [a]). It is a bit sad, but I think that's The Curse of The _|_, which infects any attempt to add static assurance. It's nicer if static properties have static witnesses, and involve no runtime activity. Maybe The Curse doesn't infect everything. What methods of assuring static properties in GHC have static witnesses? I think no: GADTs, lightweight static capabilities, forall a . [a] trick, nested/non-regular types I think yes: associated types, class constraints You have a type (NonEmpty (NonEmpty a)). If you expand that out, I think you get a forall n1. List (forall n2. List a n2) n1 So you're instantiating the element type of the outer list with a polytype, which requires impredicativity too, not just existentials! It's true, but that seems to work without a hiccup right now Jim ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Rank-2 polymorphism and pattern matching
On Jan 4, 2008 5:15 AM, Simon Peyton-Jones [EMAIL PROTECTED] wrote:
| The following won't compile for me
|
| isnull :: (forall a . [a]) - Bool
| isnull ([] :: forall b . [b]) = True
|
| Couldn't match expected type `forall b. [b]'
| against inferred type `[a]'
| In the pattern: []
This is a pretty strange thing to do, to match a polymorphic argument against
a data constructor. I guess you'd expect this to work too, perhaps?
f :: forall a. (forall b. Either a b) - a
f (Left x) = x
I grant that arguably these should work, but I think it'd be quite tricky to
make it do so, because it'd involve re-generalising in the pattern.
Furthermore, I can't see any use for it. Just remove the type signature from
the pattern.
One could argue that it's a bad sign that the pattern typechecker should have
difficulty with this. But until it turns out to be important I'm not going
to lose sleep over it!
This is literate Haskell. It's in the LaTeX style, since my mail
reader won't change the quoting mark from ''. It is not a valid LaTeX
file.
My reason for wanting pattern matching on values of polymorphic types
is a kind of first-level refinement types. I'm going to demonstrate
using the risers function, as presented in Dana N. Xu's ESC/Haskell
(http://research.microsoft.com/Users/simonpj/papers/verify/escH-hw.ps
or http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps ), which
references Neil Mitchell's Catch
(http://www-users.cs.york.ac.uk/~ndm/catch/ ). I'll also be
referencing an example from Tim Freeman's thesis on refinement types
for ML (http://www.cs.ucla.edu/~palsberg/tba/papers/freeman-thesis94.pdf
)
\begin{code}
{-# OPTIONS -fglasgow-exts #-}
-- The LANGUAGE pragma is usually a pain for exploratory programming.
\end{code}
This is the risers function, as presented by Xu. It returns the sorted
sublists of a list. None of the lists in the return value are empty,
and if the argument is non-empty, the return value is also non-empty.
\begin{code}
risersXu :: (Ord t) = [t] - [[t]]
risersXu [] = []
risersXu [x] = [[x]]
risersXu (x:y:etc) =
let ss = risersXu (y : etc)
in case x = y of
True - (x : (head ss)) : (tail ss)
False - ([x]) : ss
\end{code}
Xu uses head and tail. These are safe here by a proof created by ESC/Haskell.
Here is the risers function according to Mitchell:
\begin{code}
risersMitchell :: Ord a = [a] - [[a]]
risersMitchell [] = []
risersMitchell [x] = [[x]]
risersMitchell (x:y:etc) = if x = y
then (x:s):ss
else [x]:(s:ss)
where (s:ss) = risersMitchell (y:etc)
\end{code}
The unsafe part here is the pattern in the where clause. Mitchell
presents a tool to prove this safe.
These unsafe operations depend on the second property of the function:
non-null inputs generate non-null outputs. We could write a type for
this functions using a trusted library with phantom types for branding
(http://okmij.org/ftp/Computation/lightweight-dependent-typing.html ).
This technique (called lightweight static capabilities) can do this
and much else, as well, but clients lose all ability to pattern match
(even in case). We could also write a type signature guaranteeing this
by using GADTs. Without either one of these, incomplete pattern
matching or calling unsafe head and tail on the result of the
recursive call seems inevitable.
Here's another way to write the function which does away with the need
for second property on the recursive call, substituting instead the
need for the first property, that no lists in the return value are
empty:
\begin{code}
risersAlt :: (Ord t) = [t] - [[t]]
risersAlt [] = []
risersAlt (x:xs) =
case risersAlt xs of
[] - [[x]]
w@((y:ys):z) -
if x = y
then (x:y:ys):z
else ([x]):w
([]:_) - error risersAlt
\end{code}
The error is never reached.
Though ensuring the second property with our usual types seems tricky,
ensuring the first is not too tough:
\begin{code}
type And1 a = (a,[a])
risersAlt' :: Ord a = [a] - [And1 a]
risersAlt' [] = []
risersAlt' (x:xs) =
case risersAlt' xs of
[] - [(x,[])]
w@(yys:z) -
if x = fst yys
then (x,fst yys : snd yys):z
else (x,[]):w
\end{code}
It is now much easier to see that risers is safe: There is one pattern
match and one case, and each is simple. No unsafe functions like head
or tail are called.
It does have two disadvantages. First, the second property is still
true, but the function type does not enforce it. This means that any
other callers of risers may have to use incomplete pattern matching or
unsafe functions, since they may not be so easy to transform. It is my
intuition that it is not frequently the case that these functions are
tricky to transform, but perhaps Neil Mitchell disagrees. We could fix
this by writing another risers function with type And1 a - And1 (And1
a), but this brings us to the
Rank-2 polymorphism and pattern matching
The following won't compile for me isnull :: (forall a . [a]) - Bool isnull ([] :: forall b . [b]) = True Couldn't match expected type `forall b. [b]' against inferred type `[a]' In the pattern: [] Wrapping it in a constructor doesn't help, though I can define a null: data NullList = NullList (forall a . [a]) null = NullList [] isnull2 :: NullList - Bool isnull2 (NullList []) = True Why? Jim ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell-cafe] Re: [Haskell] Swapping parameters and type classes
On 9/18/07, Simon Marlow [EMAIL PROTECTED] wrote: Ian Lynagh wrote: I proposed renaming haskell@ - haskell-announce@ haskell-cafe@ - haskell@ [snip] but now I have to admit I think haskell-cafe is a big win for the community. To me this suggests renaming haskell@ to haskell-announce@ while leaving haskell-cafe@ as is. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[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-cafe] Using GADTs
{-# OPTIONS -fglasgow-exts #-}
module NNF where
The way I would do this would be to encode as much of the value as I
cared to in the constructors for concepts, rather than just encoding
the top-level constructor.
data Named
data Equal a b
data Negation a
data Top
data Concept t where
CNamed :: String - Concept Named
CEqual :: Concept a - Concept b - Concept (Equal a b)
CNegation:: Concept a - Concept (Negation a)
CTop :: Concept Top
Then, I could form a datatype that does not contain a Concept, but
merely certifies that all Concepts of a certain type are in NNF.
data NNF x where
NNFnamed :: NNF Named
NNFequal :: NNF a - NNF b - NNF (Equal a b)
NNFnegateName :: NNF (Negation Named)
NNFnegateTop :: NNF (Negation Top)
Now I have a generic constructor for some Concept of NNF, value
unknown, that encodes a concept and a proof of its NNF-ness.
data NNFConcept = forall t . NNFConcept (Concept t) (NNF t)
And I take a Concept with some value, transform its value somehow, and
get an NNF concept.
nnf :: Concept t - NNFConcept
nnf (CNamed x) = NNFConcept (CNamed x) NNFnamed
nnf (CEqual x y) =
case (nnf x, nnf y) of
(NNFConcept a a', NNFConcept b b') -
NNFConcept (CEqual a b) (NNFequal a' b')
nnf (CNegation (CEqual x y)) =
case (nnf (CNegation x), nnf (CNegation y)) of
(NNFConcept a a', NNFConcept b b') -
NNFConcept (CEqual a b) (NNFequal a' b')
The above function is not total, even for the limited subset of
Concepts discussed above.
By the way, the code you included last time did not compile. I think
you'll probably get a quicker response than my lazy two-day turnaround
if you make sure to run your posted code through Your Favorite
Compiler first.
Hope this helps,
Jim
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Constraints on data-types, mis-feature?
On 7/9/07, Jonathan Cast [EMAIL PROTECTED] wrote: GADTs don't change anything (at least, not the last time I checked). GHC (in HEAD, at least) eliminates this wart for any datatype declared with GADT syntax. http://www.haskell.org/ghc/dist/current/docs/users_guide/data-type-extensions.html#gadt-style Any data type that can be declared in standard Haskell-98 syntax can also be declared using GADT-style syntax. The choice is largely stylistic, but GADT-style declarations differ in one important respect: they treat class constraints on the data constructors differently. Specifically, if the constructor is given a type-class context, that context is made available by pattern matching. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] reading existential types
reading existentials (or gadts, for that matter) is an interesting problem. sometimes too interesting.. http://www.padsproj.org/ is a project that allows automated reading codde for even some dependently-typed data. Perhaps it has something to offer for automatic deriving of Read instances for GADTs? Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Church Encoding Function
On 3/10/07, Robert Dockins [EMAIL PROTECTED] wrote: I'm pretty sure you can define a catamorphism for any regular algebraic data type. I'm not 100% sure what the story is for non-regular (AKA nested) datatypes. They do exist: Initial Algebra Semantics is Enough! Patricia Johann and Neil Ghani. http://crab.rutgers.edu/~pjohann/tlca07.pdf code: http://www.cs.nott.ac.uk/~nxg/Tlca07.hs Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type-level lambdas in Haskell? ( was Multiparameter class error)
On 2/21/07, Alfonso Acosta [EMAIL PROTECTED] wrote: In my opinion adding Type-level lambdas would be the way to go, but they unfortunately are not part of Haskell. [snip] Is there any extension to the language covering type-level lambdas or even a plan to include them in next revision? SPJ suggested that type lambdas aren't in GHC because they unification for type inference impossible: http://www.mail-archive.com/haskell@haskell.org/msg10623.html The feature list for EHC indicates that it does support type lambdas, though I haven't tested this: http://www.cs.uu.nl/wiki/Ehc/LanguageFeatures A History of Haskell: http://research.microsoft.com/~simonpj/papers/history-of-haskell/index.htm points to A system of constructor classes http://web.cecs.pdx.edu/~mpj/pubs/fpca93.html or http://citeseer.ist.psu.edu/jones95system.html regarding unification and type lambdas. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Programming an Evaluation Context
On 2/14/07, Klaus Ostermann [EMAIL PROTECTED] wrote: in structural operational semantics, an evaluation context is often used to decompose an expression into a redex and its context. Have you seen http://citeseer.ist.psu.edu/mcbride01derivative.html The Derivative of a Regular Type is its Type of One-Hole Contexts Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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-cafe] Re: Higher kinds (and impredicativity?)
On 1/16/07, Chung-chieh Shan [EMAIL PROTECTED] wrote: in particular, if a type is well-kinded (i.e., well-formed) then it should either be a value type (such as [Int] and forall a. a) or contain a redex (such as (\a - a) Int). I think I see. I was expecting that (forall v : k . t)@s could beta-reduce to (forall v : k . [EMAIL PROTECTED]), which in retrospect seems greedy. :-) Thanks, Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher kinds (and impredicativity?)
On 1/15/07, Doaitse Swierstra [EMAIL PROTECTED] wrote: Values that live as elements in data have to be data themselves, and thus have to be of a type that has kind *. But the example I give doesn't have a value of kind * - * living in data. The constructor is nullary, only the parameter to the type is not of kind *. This is fine in declarations like: data Good (x :: * - *) where Good :: Good Maybe What I'm asking is why, for declarations like data OK (x :: * - *) where OK :: OK x type Fine = OK Maybe type Evil = OK (forall (f :: * - *) . f) Fine is allowed, while Evil is not. This is not the case for data OK' (x :: *) where OK' :: OK' x type Fine' = OK' Maybe type Evil' = OK' (forall (f :: *) . f) When both Fine' and Evil' are accpeted. Jim On Jan 15, 2007, at 3:39 AM, Jim Apple wrote: Why is this declaration ill-formed: data Bad t where Bad :: Bad (forall (f :: * - *) . f) GHC 6.6 says: `f' is not applied to enough type arguments Expected kind `*', but `f' has kind `* - *' In the type `forall f :: (* - *). f' In the type `Bad (forall f :: (* - *). f)' In the data type declaration for `Bad' I suppose this is because the kind inference rule is C, x : k1 |- y : * --- C |- (\forall x : k1 . y) : * I'd expect C, x : k1 |- y : k2 --- C |- (\forall x : k1 . y) : k2 Is there a foundational or an implementation reason for this restriction? Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher kinds (and impredicativity?)
On 1/15/07, Jim Apple [EMAIL PROTECTED] wrote: data OK' (x :: *) where OK' :: OK' x type Fine' = OK' Maybe type Evil' = OK' (forall (f :: *) . f) Correction: that Maybe should obviously be something of kind *, like Bool. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Higher kinds (and impredicativity?)
On 1/15/07, Chung-chieh Shan [EMAIL PROTECTED] wrote: I consider it a foundational reason. You seem to want (forall (f :: * - *) . f) to have kind * - *. But that means that I should be able to apply it to a type, say Int, to get a type (forall (f :: * - *) . f) Int. What values inhabit this type? The same ones that inhabit (forall (f :: * - *) . f Int); that is, none (or _|_). I don't see the uninhabitability of a type as reason why the type itself should be ill-formed, even in a domain without lifted types. For instance, (Int - (forall a . a)) should be a valid type even in a system where it is not inhabited, because I want to be able to write the type ((Int - (forall a . a)) - (forall b . b)), which is inhabited. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Higher kinds (and impredicativity?)
Why is this declaration ill-formed: data Bad t where Bad :: Bad (forall (f :: * - *) . f) GHC 6.6 says: `f' is not applied to enough type arguments Expected kind `*', but `f' has kind `* - *' In the type `forall f :: (* - *). f' In the type `Bad (forall f :: (* - *). f)' In the data type declaration for `Bad' I suppose this is because the kind inference rule is C, x : k1 |- y : * --- C |- (\forall x : k1 . y) : * I'd expect C, x : k1 |- y : k2 --- C |- (\forall x : k1 . y) : k2 Is there a foundational or an implementation reason for this restriction? Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Are GADTs expressive? Simple proof-carrying code in Haskell98
On 1/13/07, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote: The shown GADT encoding seems to be of the kind that is convertible to typeclasses in the straightforward way, see for example, http://pobox.com/~oleg/ftp/Haskell/GADT-interpreter.hs See also Conor McBride's Faking It: Simulating Dependent Types in Haskell http://citeseer.ist.psu.edu/mcbride01faking.html Also, GADTs are extensible in GHC HEAD, though type classes are still necessary to write functions on them: http://haskell.org/haskellwiki/GHC/Indexed_types#Instance_declarations Incidentally, the typeclass encoding has an advantage: If the submitted proof is invalid, the error will be reported at compile time. [more snipped] I don't quite understand what you're getting at here. Is it that with the GADT approach, one could write Terminating (Apply omega omega) (undefined) (undefined) and the typechecker would not complain? That certainly is an issue, but I think you're saying something deeper that I'm not getting. However, it seems that the problem at hand admits a far simpler solution -- in Haskell98. The solution is in spirit of lightweight static capabilities. Here it is: module PCC (Terminates, -- data constructor is not exported make_terminates, get_term) where [snip] The module PCC constitutes the `trusted kernel' with respect to the Terminates datatype. The function make_terminates must be rigorously verified in order to deserve our trust. But the same should be said for the GADT or any other solution: e.g., one can easily add a new case alternative to the Normal datatype declaring Omega to be in the normal form. That's true, but there is at least one disadvantage to the PCC module: some functions manipulating terminating terms must be placed inside the trusted core. This is not the case with GADTs. For instance, we could write a term that takes a non-normalized (but terminating) term and beta-reduces it once to return a new normalizing term. We can't do this as a mere client of the PCC module without calling make_terminates again. Operations on types with hidden constructors sometimes have to be put in the trusted core. This was a small cost for terminating terms in the untyped lambda calculus, but it's a bigger cost for other structures. This is sort of like writing nested types for balanced trees vs. using Data.Set. Data.Set does guarantee that the tree is balanced, but we can only believe this after looking at each function in Data/Set.hs. Yes, the definition for balanced nested trees must be written with the same care as the functions in Data.Set, but there are a lot more functions in Data.Set Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
On 1/8/07, Tomasz Zielonka [EMAIL PROTECTED] wrote: On Mon, Jan 08, 2007 at 08:02:36AM -0500, Lennart Augustsson wrote: So it sounds to me like the (terminating) type checker solves the halting problem. Can you please explain which part of this I have misunderstood? Perhaps you, the user, have to encode the proof of halting in the way you construct the term? The Terminating datatype takes three parameters: 1. A term in the untyped lambda calculus 2. A sequence of beta reductions 3. A proof that the result of the beta reductions is normalized. Number 2 is the hard part. For a term that calculated the factorial of 5, the list in part 2 would be at least 120 items long, and each one is kind of a pain. GHC's type checker ends up doing exactly what it was doing before: checking proofs. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
On 1/8/07, Robin Green [EMAIL PROTECTED] wrote: On Mon, 8 Jan 2007 08:51:40 -0500 Jim Apple [EMAIL PROTECTED] wrote: GHC's type checker ends up doing exactly what it was doing before: checking proofs. Well, not really - or not the proof you thought you were getting. As I am constantly at pains to point out, in a language with the possibility of well-typed, non-terminating terms, like Haskell, what you actually get is a partial proof - that *if* the expression you are demanding terminates, you will get a value of the correct type. Of course. Were there a recursion-free dialect of Haskell, it could be typecheck/proofcheck the Terminating datatype, though it would be useless for doing any actual work. Proof assistants like Coq can solve this dilemma, and so can languages in the Dependent ML family, by allowing non-terminating programs but only terminating proofs, and by proving termination by well-founded induction. Nobody should think Haskell+GADTs provides the sort of assurances that these can. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad Set via GADT
On 1/3/07, Roberto Zunino [EMAIL PROTECTED] wrote: 1) Why the first version did not typececk? 2) Why the second one does? 3) If I replace (Teq a w) with (Teq w a), as in SM :: Ord w = Teq w a - Set.Set w - SetM a then union above does not typecheck! Why? I guess the type variable unification deriving from matching Teq is not symmetric as I expect it to be... These are very interesting questions that I forgot about until reminded by Haskell Weekly News. Thanks, HWN! 1) Class constraints can't be used on pattern matching. They ARE restrictive on construction, however. This is arguably bug in the Haskell standard. It is fixed in GHC HEAD for datatypes declared in the GADT way, so as not to break H98 code: http://article.gmane.org/gmane.comp.lang.haskell.cvs.all/29458/match=gadt+class+context 2) The second one works because Class constraints can be used when pattern matching existentials. 3) I imagine this might have something to do with the coercions that System FC uses. With one ordering, a coercion might occur that in another one is unnecessary. This coercion might allow the use of Ord w by using it before the coercion from S.Set a to S.Set w. #3 is just a guess. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] GADTs are expressive
To show how expressive GADTs are, the datatype Terminating can hold
any term in the untyped lambda calculus that terminates, and none that
don't. I don't think that an encoding of this is too surprising, but I
thought it might be a good demonstration of the power that GADTs
bring.
{-# OPTIONS -fglasgow-exts #-}
{- Using GADTs to encode normalizable and non-normalizable terms in
the lambda calculus. For definitions of normalizable and de Bruin
indices, I used:
Christian Urban and Stefan Berghofer - A Head-to-Head Comparison of
de Bruijn Indices and Names. In Proceedings of the International
Workshop on Logical Frameworks and Meta-Languages: Theory and
Practice (LFMTP 2006). Seattle, USA. ENTCS. Pages 46-59
http://www4.in.tum.de/~urbanc/Publications/lfmtp-06.ps
@incollection{ pierce97foundational,
author = Benjamin Pierce,
title = Foundational Calculi for Programming Languages,
booktitle = The Computer Science and Engineering Handbook,
publisher = CRC Press,
address = Boca Raton, FL,
editor = Allen B. Tucker,
year = 1997,
url = citeseer.ist.psu.edu/pierce95foundational.html
}
-}
module Terminating where
-- Terms in the untyped lambda-calculus with the de Bruijn representation
data Term t where
Var :: Nat n - Term (Var n)
Lambda :: Term t - Term (Lambda t)
Apply :: Term t1 - Term t2 - Term (Apply t1 t2)
-- Natural numbers
data Nat n where
Zero :: Nat Z
Succ :: Nat n - Nat (S n)
data Z
data S n
data Var t
data Lambda t
data Apply t1 t2
data Less n m where
LessZero :: Less Z (S n)
LessSucc :: Less n m - Less (S n) (S m)
data Equal a b where
Equal :: Equal a a
data Plus a b c where
PlusZero :: Plus Z b b
PlusSucc :: Plus a b c - Plus (S a) b (S c)
{- We can reduce a term by function application, reduction under the lambda,
or reduction of either side of an application. We don't need this full
power, since we could get by with normal-order evaluation, but that
required a more complicated datatype for Reduce.
-}
data Reduce t1 t2 where
ReduceSimple :: Replace Z t1 t2 t3 - Reduce (Apply (Lambda t1) t2) t3
ReduceLambda :: Reduce t1 t2 - Reduce (Lambda t1) (Lambda t2)
ReduceApplyLeft :: Reduce t1 t2 - Reduce (Apply t1 t3) (Apply t2 t3)
ReduceApplyRight :: Reduce t1 t2 - Reduce (Apply t3 t1) (Apply t3 t2)
{- Lift and Replace use the de Bruijn operations as expressed in the Urban
and Berghofer paper. -}
data Lift n k t1 t2 where
LiftVarLess :: Less i k - Lift n k (Var i) (Var i)
LiftVarGTE :: Either (Equal i k) (Less k i) - Plus i n r - Lift
n k (Var i) (Var r)
LiftApply :: Lift n k t1 t1' - Lift n k t2 t2' - Lift n k (Apply
t1 t2) (Apply t1' t2')
LiftLambda :: Lift n (S k) t1 t2 - Lift n k (Lambda t1) (Lambda t2)
data Replace k t n r where
ReplaceVarLess :: Less i k - Replace k (Var i) n (Var i)
ReplaceVarEq :: Equal i k - Lift k Z n r - Replace k (Var i) n r
ReplaceVarMore :: Less k (S i) - Replace k (Var (S i)) n (Var i)
ReplaceApply :: Replace k t1 n r1 - Replace k t2 n r2 - Replace
k (Apply t1 t2) n (Apply r1 r2)
ReplaceLambda :: Replace (S k) t n r - Replace k (Lambda t) n (Lambda r)
{- Reflexive transitive closure of the reduction relation. -}
data ReduceEventually t1 t2 where
ReduceZero :: ReduceEventually t1 t1
ReduceSucc :: Reduce t1 t2 - ReduceEventually t2 t3 -
ReduceEventually t1 t3
-- Definition of normal form: nothing with a lambda term applied to anything.
data Normal t where
NormalVar :: Normal (Var n)
NormalLambda :: Normal t - Normal (Lambda t)
NormalApplyVar :: Normal t - Normal (Apply (Var i) t)
NormalApplyApply :: Normal (Apply t1 t2) - Normal t3 - Normal
(Apply (Apply t1 t2) t3)
-- Something is terminating when it reduces to something normal
data Terminating where
Terminating :: Term t - ReduceEventually t t' - Normal t' - Terminating
{- We can encode terms that are non-terminating, even though this set is
only co-recursively enumerable, so we can't actually prove all of the
non-normalizable terms of the lambda calculus are non-normalizable.
-}
data Reducible t1 where
Reducible :: Reduce t1 t2 - Reducible t1
-- A term is non-normalizable if, no matter how many reductions you
have applied,
-- you can still apply one more.
type Infinite t1 = forall t2 . ReduceEventually t1 t2 - Reducible t2
data NonTerminating where
NonTerminating :: Term t - Infinite t - NonTerminating
-- x
test1 :: Terminating
test1 = Terminating (Var Zero) ReduceZero NormalVar
-- (\x . x)@y
test2 :: Terminating
test2 = Terminating (Apply (Lambda (Var Zero))(Var Zero))
(ReduceSucc (ReduceSimple (ReplaceVarEq Equal (LiftVarGTE
(Left Equal) PlusZero))) ReduceZero)
NormalVar
-- omega = [EMAIL PROTECTED]
type Omega = Lambda (Apply (Var Z) (Var Z))
omega = Lambda (Apply (Var Zero) (Var Zero))
-- (\x . \y . y)@([EMAIL PROTECTED])
test3 :: Terminating
test3 = Terminating (Apply (Lambda (Lambda (Var Zero))) omega)
(ReduceSucc (ReduceSimple
[Haskell-cafe] Re: Red-black trees as a nested datatype
Correction: type RedBlackTree a = Tree a -- A red tree with two levels of black nodes is just a red node on -- top of two two-level black nodes. (Node a (Black2 a)) (Black2 a) a () type RedBlackTree a = Tree a -- A red tree with two levels of black nodes is just a red node on -- top of two black nodes. (Node (Black2 a) a) (Black2 a) a () ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haskell Weekly News: December 12, 2006
On 12/12/06, Donald Bruce Stewart [EMAIL PROTECTED] wrote: --- Haskell Weekly News http://sequence.complete.org/ Issue 53 - December 12, 2006 --- [snip] Quotes of the Week * Jim Apple: The Haskell list probably has the widest 'knowledge bandwidth' of any mailing list I've ever seen, from total beginner questions to highly abstruse stuff which probably represents the cutting edge of PhD research. All are answered with detail and good humour. I like that quote, but I'm an American, so I think they're answered with good humor. The quote looks like it is from http://www.oreillynet.com/mac/blog/2006/03/haskell_vs_ocamlwhich_do_you_p.html#comment-23152 , and the attributions are actually beneath, rather than above, the quotes. The true author is Jeremy O'Donoghue. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A type class puzzle
On 11/2/06, Yitzchak Gale [EMAIL PROTECTED] wrote: GHC says: Functional dependencies conflict between instance declarations: instance Replace Zero a a (a - a - a) instance (...) = Replace (Succ n) a [l] f' Not true. The type constraints on the second instance prevent any overlap. GHC doesn't take constraints into account when checking fundeps. You're looking for Sulzmann's Chameleon, which does all sorts of constraint magic. http://www.comp.nus.edu.sg/~sulzmann/chameleon/ Also, I'd be surprized if Oleg didn't have a work-around in GHC. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Automatic fixity allocation for symbolic operators
On 10/14/06, Brian Hulley [EMAIL PROTECTED] wrote: User defined fixities are an enormous problem for an interactive editor This is the second or third time you've proposed a language change based on the editor you're writing. I don't think this is a fruitful avenue. There are three ways to change Haskell's lexical structure: 1. DIY on an open-source compiler/interpreter of your choice. 2. Write your own compiler/interpreter. 3. Get the change into Haskell''. If the Haskell'' procedure is like the Haskell' procedure, you'll have to do 1 or 2 before you do 3. It's possible that you will convince someone that your syntax changes are worth doing, and that this person will do step 1 or step 2 for you, but I don't think so. I haven't done the research myself, but I think if you look at the source control logs for Your Favorite Haskell Compiler/interpreter and the HCAR, you will find very few commits/projects devoted to syntax. I think this is because Haskellers are much more interested in semantics. Proposing changes that break existing code or segment the Haskell code base just doesn't seem like a win. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] GHC Core still supported?
In http://www.haskell.org/ghc/dist/current/docs/users_guide/ext-core.html
, I see two notes that I can't verify:
1. I don't see any CORE pragma on
http://www.haskell.org/ghc/dist/current/docs/users_guide/pragmas.html
2. Using GHC 6.5.20060920, I compile
module Core where
data Foo = Bar
with -fext-core to get
%module main:Core
%data main:Core.Foo =
{Bar};
I then compile the resulting hcr file with no flags to get
no location info:
1: Parse error
:
%data main:Core.Foo =
{Bar};
Jim
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: irrefutable patterns for existential types / GADTs
On 9/30/06, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote:
data Eq a b where Refl :: Eq a a
coerce :: Eq a b - a - b
coerce ~Refl x = x
But this works well with Leibniz-style equality (
http://homepage.mac.com/pasalic/p2/papers/thesis.pdf ), because the
Equality proof/term is actually used:
data Equal a b = Equal (forall f . f a - f b)
newtype Id x = Id { unId :: x}
coerce :: Equal a b - a - b
coerce ~(Equal f) x = unId (f (Id x))
Jim
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Non-existant existential?
Consider the following: data SimpExist a = SimpExist (forall x . x - a) f :: SimpExist Bool f = SimpExist (const True) g = SimpExist id What is the type of g? In a similar example, GHC tells me it is of type SimpExist c. Yet, I can't unify it with any other SimpExist c'. It seems to me that this is something like exists x . SimpExist x, and is similar to: data ExistWrap = forall a . ExistWrap (forall x . x - a) Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-existant existential?
On 9/21/06, Bruno Oliveira [EMAIL PROTECTED] wrote: Have you tried to type check this example (the g)? No. Please excuse me, as I wasn't by my GHC at the time. Let's try: data SimpExist a = Base a | SimpExist (SimpExist (forall x . x - a)) g :: SimpExist (forall a . a - a) g = Base id h = SimpExist g data WrapExist = forall a . WrapExist (SimpExist a) i = WrapExist h I'm familiar with the use for forall to mean exists, but I am baffled by h's ineffable type! Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Non-existant existential?
When I look at the generated core, I see that both h and same = Base undefined have the same type: %forall a . main:Fonly.SimpExist a I'm using GHC 6.5.20060819. If this is a bug, I actually find it kind of useful, for reasons I can elaborate later. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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
Re: [Haskell-cafe] Re: map (-2) [1..5]
See also: torsors http://math.ucr.edu/home/baez/torsors.html Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The difficulty of designing a sequence class
On 7/31/06, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote: G'day all. Quoting David Menendez [EMAIL PROTECTED]: That's a tough call to make. Changing the kind of Sequence to * from * - * means losing the Functor, Monad, and MonadPlus superclasses and all the various maps and zips. Perhaps Functor/Monad/etc are the culprits here. Indeed. See Oleg's message from a few months back where he shows that we can get John Hughes Restricted Data Types (Set is a Monad) by adding parameters to type classes: http://www.haskell.org//pipermail/haskell-prime/2006-February/000498.html http://hackage.haskell.org/trac/haskell-prime/ticket/98 Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: collecting requirements for FDs
On 4/10/06, Ross Paterson [EMAIL PROTECTED] wrote: What other libraries should Haskell' support, and what are their requirements? http://hackage.haskell.org/trac/ghc/wiki/CollectionClassFramework There are two range arguments here, IIUC. Jim ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: bringing discussions to a close
On 3/29/06, Simon Peyton-Jones [EMAIL PROTECTED] wrote: Proposal: make all pattern bindings completely monomorphic (regardless of type signatures) ... My bet is that this is a feature that is tricky to implement, but which is virtually never used. If this proposal is implemented, is there a workaround for cases where it is used? Jim ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: bringing discussions to a close
On 3/28/06, isaac jones [EMAIL PROTECTED] wrote: The only topics that should remain open are concurrency and the class system. What happene to bullet 3, perhaps standard libraries? Jim ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: supertyping
Has this list yet discussed John's supertyping proposal? http://repetae.net/john/recent/out/supertyping.html Jim ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
[Haskell-cafe] Equirecursive types?
According to Pierce's book, O'Caml has an optional equirecursive type extension that turns off the occurs check. Is there any particular reason Haskell doesn't have that available? Here's what got me thinking about it: http://lambda-the-ultimate.org/node/1360#comment-15656 Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Collections interface
I have created a ticket to make a standard collection interface. It is here: http://hackage.haskell.org/trac/haskell-prime/ticket/97 Obviously, it will be tough to figure out what the library can look like without knowing what MPTC's will look like. Jim ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: Restricted Data Types Now
On 2/8/06, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote: It seems we can emulate the restricted data types in existing Haskell. I have proposed this for Haskell' libraries. See http://hackage.haskell.org/trac/haskell-prime/ticket/98 Jim ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
[Haskell-cafe] Haskell documentation and GADTs
I'm having trouble generating automatic documentation in a module with GADTs. Haddock gives a parse error, and http://www.cse.ogi.edu/~hallgren/Programatica/tools/features.html seems to indicate that Programmatica will as well. Any ideas? Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: instance Functor Set, was: Re: Export lists in modules
On 3/1/06, Johannes Waldmann [EMAIL PROTECTED] wrote: But my point was that I want to use do notation for Sets (in fact, for any kind of collection) so I'd need the original Functor and Monad. I understand this for Monad. Why not just redefine Functor, Oleg-style? I couldn't use ghc's Rebindable Syntax feature because the types for (=) would not match? http://www.haskell.org/ghc/docs/6.4/html/users_guide/syntax-extns.html#rebindable-syntax Good news, everyone! http://www.haskell.org/ghc/dist/current/docs/users_guide/syntax-extns.html#rebindable-syntax That looks good to me! Jim ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: instance Functor Set, was: Re: Export lists in modules
On 2/28/06, Johannes Waldmann [EMAIL PROTECTED] wrote:
Malcolm Wallace wrote:
But if contexts-on-datatypes worked correctly,
data Set a = Ord a =
then even the real map from Data.Set:
map :: (Ord a, Ord b) = (a - b) - Set a - Set b
could be an instance method of Functor.
I'd love that. But I don't quite understand:
do you think this is/should be possible with:
current Haskell? Haskell-Prime? Current ghc (what extensions)?
as Oleg:
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
module Map where
import qualified Data.Set
class MyMap f a b where
myMap :: (a - b) - f a - f b
instance (Functor f) = MyMap f a b where
myMap = fmap
instance (Ord a, Ord b) = MyMap Data.Set.Set a b where
myMap = Data.Set.map
Jim
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
[Haskell-cafe] Re: libreadline dependency
J. Scott Thayer, M.D. wrote: Haskell wants libreadline 4 while I have libreadline 5. I'm not sure about SUSE, but Fedora has libreadline_compat packages. HTH, Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
exported pattern matching
Sometimes I'd like to use a smart constructor but have pattern matching as well. There has been talk elsewhere of allowing export of data constructors for /matching/ but not for /construction/: module One- data Picky a = Nil | One a picky x = if some_complex_thing x then One x else Nil module Two- f x = g $ picky x g Nil y = y g (One x) y = x h Nil = One True - I'd like for the function g to be fine and the function h to get a complaint like error: no constructor 'One' or, even better, error: 'One' only works in pattern matching Jim ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Restricted Data Types
Have we considered Restricted Data Types? http://www.cs.chalmers.se/~rjmh/Papers/restricted-datatypes.ps Or even absracting over contexts, as described in section 7.5 (p. 14/15) of the above? Jim ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
CHRs, was Re: MPTCs and functional dependencies
... read the JFP journal submission that Martin Sulzmann and Peter Stuckey and I have been working on. http://research.microsoft.com/%7Esimonpj/papers/fd-chr Has this list discussed using CHRs instead of fundeps? Jim ___ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime
Re: cvs commit: fptools/libraries/base/Data IntMap.hs Map.hs Sequence.hs Set.hs fptools/libraries/base/Data/Generics Instances.hs Twins.hs
Simon Peyton Jones wrote: simonpj 2006/01/06 07:51:23 PST Modified files: libraries/base/Data IntMap.hs Map.hs Sequence.hs Set.hs libraries/base/Data/Generics Instances.hs Twins.hs Log: Eta-expand some higher-rank functions. GHC is about to move to *invariant* rather than *contra-variant* in function arguments, so far as type subsumption is concerned. These eta-expansions are simple, and allow type inference to go through with invariance. Why drop contra-variace? Jim ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
[Haskell-cafe] Re: [darcs-conflicts] how to nicely implement phantom type coersion?
Ralf Hinze wrote: the type a :=: b defined below goes back to Leibniz's principle of substituting equals for equals: If you like this, check out two of Ralf's papers: First-class phantom types: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2003-1901 Fun with phantom types: http://www.informatik.uni-bonn.de/~ralf/publications/With.pdf The first (in section 2.4) explains a limitation of :=: I highly recommend both papers. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Data.Typeable and default instances
{-# OPTIONS -fglasgow-exts #-}
import Maybe
import Data.Typeable
data Nil = Nil deriving (Eq,Typeable,Show)
class (Typeable t) = List a t where
init :: (t - b) - (forall y . (List a y) = y - b)
init f z = fromJust $ do x - cast z
return $ f x
instance List a Nil where
Could not deduce (List a1 y)
from the context (List a Nil, Typeable Nil, List a y)
arising from use of `Main.$dminit' at Main.hs:21:0
Probable fix: add (List a1 y) to the class or instance method
`Main.init'
In the definition of `init': init = Main.$dminit
In the definition for method `Main.init'
In the instance declaration for `List a Nil'
but copying and pasting the code from init to the instance declaration
works fine.
Jim
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Associated types in 6.6?
Simon Peyton-Jones wrote: The trick lies in coming up with a suitable typed intermediate representation for the program -- System F isn't enough. Is that because GHC's TIL is not exactly System F? As ever, we tend to work harder on things that folk appear to want; Unrelated question: will boxy types allow forall-quantified types in instance declarations? so anyone who is keen on associated types, do sing out and describe your application a bit. If yes, I'll clean-up and send out some code showing what I think would be a good use. Jim ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Rebindable monads?
Where is there documentation for rebindable syntax for monads with class constraints: (=) :: (Foo m, Baz a) = m a - (a - m b) - m b http://article.gmane.org/gmane.comp.lang.haskell.cvs.ghc/9447/match=syntax The users guide seems to disallow such type signatures: http://haskell.org/ghc/docs/latest/html/users_guide/syntax-extns.html#rebindable-syntax Jim ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Associated types in 6.6?
I see that associated types is already in CVS: http://article.gmane.org/gmane.comp.lang.haskell.cvs.all/19423/match=associated Will it be in 6.6? Jim ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
[Haskell-cafe] Re: Dataflow and Comonads was Re: Monads in Scala, ...
Shae Matijs Erisson wrote: I do wish I could find the source code from this paper online, I'd rather not type it in by hand. Do researchers usually manually transcribe code? Both Evince and Acrobat Reader can copy text. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
GHC 6.6
Help build the anticipation: http://haskell.org/hawiki/GHC_206_2e6 Present text: GHC 6.6: Will be out before May 2006. Included: * Parallel GHC * Associated types with class Maybe: * Impredicativity * GADT Typeclass interaction * Data types as kinds No: Jim ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
[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
Re: ANNOUNCE: GHC survey results
Some people would like features removed (implicit parameters was mentioned a couple of times). Linear implicit parameters is a clear candidate for removal. I don't understand the motivation for this. Implicit parameters do weird things with the monomorphism restriction, but when I'm worried about that, I choose not to use them together. Why remove a feature from a product? Why not, instead, just choose to not use it? Jim ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
[Haskell-cafe] Buddha and GHC 6.4
Has anyone gotten Buddha (now called plargleflarp http://www.cs.mu.oz.au/~bjpop/buddha/) do work with GHC 6.4? I'm getting ghc-6.4: unknown package: buddha Jim P.S. What happened to the old name? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: cvs commit: fptools/ghc/compiler/hsSyn HsUtils.lhs fptools/ghc/compiler/typecheck TcRnDriver.lhs TcRnMonad.lhs TcUnify.lhs
Simon Peyton Jones wrote: - For command-line 'let' and 'x-e' forms, if exactly one variable is bound, we print its value if it is Showable and not () prompt let x = 4 4 prompt x - return 5 5 prompt let ones = [1:x] What am I to do if I want ones set, but not printed? Jim ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
[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] 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: 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
Re: gfindtype type
Let me restate: gfindtype's declaration should be gfindtype :: (Data x, Typeable y) = x - Maybe y Jim ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
gfindtype type
Why is gfindtype :: (Data x, Data y) = x - Maybe y and not gfindtype :: (Data x, Typeable y) = x - Maybe y ? Jim Apple ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
[Haskell-cafe] Re: Top Level etc.
Benjamin Franksen wrote: Please note that implicit parameters -- at least as currently implemented in GHC -- have a number of severe problems. Does anyone have examples of these? This one scares the foo out of me: * It's not even safe in general to add a signature giving the same type that the compiler would infer anyway Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[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] 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
[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] 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?
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-cafe] numerical subtyping
Is there a standard Haskell trick for checking run-time assignment to data types? I'd like a data type of Probability that ensures its Double argument is between 0 and 1. Jim ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: generalised algebraic data types, existential types, and phantom types
I tried to post this to gmane.comp.lang.haskell.general, but it never
got there - it may belong here anyway.
Abraham Egnor wrote:
Is there any closer approximation [of GADTs] possible?
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
data Term a = forall b . (EqType a b, EqType b Int) = Lit Int
| forall b . (EqType a b, EqType b Int) = Inc (Term Int)
| forall b . (EqType a b, EqType b Bool) = IsZ (Term Int)
| If (Term Bool) (Term a) (Term a)
| forall b . Fst (Term (a,b))
| forall b . Snd (Term (b,a))
| forall b c . (EqType a (b,c))= Pair (Term b) (Term c)
class EqType a b | a-b, b-a
instance EqType a a
Unfortunately, I can't seem to write an eval function:
eval (Lit a) = a
gives
Inferred type is less polymorphic than expected
Quantified type variable `b' is unified with `Int'
When checking an existential match that binds
The pattern(s) have type(s): Term Int
The body has type: Int
In the definition of `eval': eval (Lit x) = x
Any ideas?
Jim
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
