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#g
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
> {-# 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
On 8/4/07, Shin-Cheng Mu <[EMAIL PROTECTED]> wrote:
> Unfortunately, unlike Omega, Haskell does not provide type
> functions.
Something similar is coming:
http://haskell.org/haskellwiki/GHC/Indexed_types#Instance_declarations_2
> Haskell does not know that Plus m n is actually
> a function and c
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
, 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 resea
levels of black nodes is just a red node on
-- top of two black nodes.
(Node (Black2 a) a) (Black2 a) a ()
-- Jim Apple
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
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 o
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 -fg
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 us
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
On 1/8/07, Roberto Zunino <[EMAIL PROTECTED]> wrote:
Does anyone else believe that using strictess annotations in GADT proof
terms would be good style?
I think Tim Sheard uses strictness in his Omega project for the same
reason you suggest. See
http://web.cecs.pdx.edu/~sheard/
Jim
___
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
unific
On 1/3/07, Roberto Zunino <[EMAIL PROTECTED]> wrote:
I tried to define a Set datatype,
with the usual operations, so that it can be made a member of the
standard Monad class.
Also, we can do this with oleg's technique of "Restricted Data Types Now":
http://article.gmane.org/gmane.comp.lang.has
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
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
; *) . 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, Ji
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
___
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
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
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 T
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?
SP
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 Gha
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
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
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
___
Haskel
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
___
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.
Perha
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
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 th
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
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
__
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 us
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 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 c
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 ov
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/mailma
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 com
Echo Nolan wrote:
1) Prove that the property holds for the null list
2) Prove that the property holds for (x:xs) under the assumption
that the property holds for xs.
As someone else said, this works for finite lists.
My question is this: what is the proof of (P([])
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.o
Shae Matijs Erisson wrote:
Please respond with any language implementations I've missed.
C++ http://www.cc.gatech.edu/~yannis/fc++/New1.5/lambda.html#monad
Jim
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/lis
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
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 phan
I downloaded and compiled buddha, but it apparently does not support
Control.Monad.State. I downloaded Hat, but it requires hmake. Hmake
fails to build (GHC 6.2.1).
Any suggestions?
Jim
___
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell
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
45 matches
Mail list logo
