[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: [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
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-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-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
[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
[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
[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
[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
[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
[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
[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-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
