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
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
{-# 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
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.
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
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
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
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
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
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
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
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
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
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
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,
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
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
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
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
---
[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
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
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
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
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:
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
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 =
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
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
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
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
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
___
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
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
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
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
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
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]
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
38 matches
Mail list logo
