Dan Doel wrote:
Implementing type inference can be very easy in a logic language,
because most of the work in a non-logic language is implementing
unification:
http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html
Correctly implementing type inference in
On Wed, Jan 13, 2010 at 7:57 AM, Peter Verswyvelen bugf...@gmail.comwrote:
A while ago, someone provided me a link to the paper Type Inference
for Overloading without Restrictions
http://www.dcc.ufmg.br/~camarao/ct-flops99.ps.gzhttp://www.dcc.ufmg.br/%7Ecamarao/ct-flops99.ps.gz
Although I
A while ago, someone provided me a link to the paper Type Inference
for Overloading without Restrictions
http://www.dcc.ufmg.br/~camarao/ct-flops99.ps.gz
Although I don't understand everything in this paper, I wander what
people's opinions are about this regarding a future Haskell language
Cristiano Paris wrote:
On Thu, Oct 8, 2009 at 12:48 PM, Lennart Augustsson wrote:
The reason a gets a single type is the monomorphism restriction (read
the report).
Using NoMonomorphismRestriction your example with a works fine.
Could you explain why, under NoMonomorphismRestriction, this
2009/10/9 wren ng thornton w...@freegeek.org:
Cristiano Paris wrote:
On Thu, Oct 8, 2009 at 12:48 PM, Lennart Augustsson wrote:
The reason a gets a single type is the monomorphism restriction (read
the report).
Using NoMonomorphismRestriction your example with a works fine.
Could you
Hi,
I'd like to know what are the typing rules used in Haskell (98 is ok).
Specifically, I'd like to know what makes
let i = \x - x in (i True, i 1)
legal, and not
let a = 1 in (a + (1 :: Int), a + (1.0 :: Float))
Is it correct that polymorphic functions can be used polymorphically
(in
minh thu wrote:
Also, I'd like to know why
id id True
is permitted but not
(\f - f f True) id
Because this requires rank-2 types:
Prelude :set -XScopedTypeVariables
Prelude :set -XRank2Types
Prelude (\(f :: forall a. a - a) - f f True) id
True
HTH,
Martijn.
minh thu wrote:
Also, I'd like to know why
id id True
is permitted but not
(\f - f f True) id
If you want to do this, answer the question what is the type of (\f -
f f True)?
You can do this, by the way, using rank-2 types:
{-# LANGUAGE Rank2Types, PatternSignatures #-}
thisIsAlwaysTrue
2009/10/8 Jochem Berndsen joc...@functor.nl:
minh thu wrote:
Also, I'd like to know why
id id True
is permitted but not
(\f - f f True) id
If you want to do this, answer the question what is the type of (\f -
f f True)?
You can do this, by the way, using rank-2 types:
{-# LANGUAGE
On Thu, Oct 8, 2009 at 11:04 AM, minh thu not...@gmail.com wrote:
Hi,
I'd like to know what are the typing rules used in Haskell (98 is ok).
Specifically, I'd like to know what makes
let i = \x - x in (i True, i 1)
legal, and not
let a = 1 in (a + (1 :: Int), a + (1.0 :: Float))
Is it
2009/10/8 Cristiano Paris fr...@theshire.org:
On Thu, Oct 8, 2009 at 11:04 AM, minh thu not...@gmail.com wrote:
Hi,
I'd like to know what are the typing rules used in Haskell (98 is ok).
Specifically, I'd like to know what makes
let i = \x - x in (i True, i 1)
legal, and not
let a = 1
The reason a gets a single type is the monomorphism restriction (read
the report).
Using NoMonomorphismRestriction your example with a works fine.
On Thu, Oct 8, 2009 at 12:29 PM, Cristiano Paris fr...@theshire.org wrote:
On Thu, Oct 8, 2009 at 11:04 AM, minh thu not...@gmail.com wrote:
Hi,
Thanks all!
Thu
2009/10/8 Lennart Augustsson lenn...@augustsson.net:
The reason a gets a single type is the monomorphism restriction (read
the report).
Using NoMonomorphismRestriction your example with a works fine.
On Thu, Oct 8, 2009 at 12:29 PM, Cristiano Paris fr...@theshire.org wrote:
On Thu, Oct 8, 2009 at 12:48 PM, Lennart Augustsson
lenn...@augustsson.net wrote:
The reason a gets a single type is the monomorphism restriction (read
the report).
Using NoMonomorphismRestriction your example with a works fine.
Could you explain why, under NoMonomorphismRestriction, this
2009/10/8 Cristiano Paris fr...@theshire.org:
On Thu, Oct 8, 2009 at 12:48 PM, Lennart Augustsson
lenn...@augustsson.net wrote:
The reason a gets a single type is the monomorphism restriction (read
the report).
Using NoMonomorphismRestriction your example with a works fine.
Could you
Hello Cristiano,
Thursday, October 8, 2009, 7:14:20 PM, you wrote:
Could you explain why, under NoMonomorphismRestriction, this typechecks:
let a = 1 in (a + (1 :: Int),a + (1 :: Float))
while this not:
foo :: Num a = a - (Int,Float)
foo k = (k + (1 :: Int), k + (1.0 :: Float))
i think
Indeed, the types
foo :: forall a . (Num a) = a - (Int, Float)
and
foo :: (forall a . (Num a) = a) - (Int, Float)
are quite different.
The first one say, I (foo) can handle any kind of numeric 'a' you (the
caller) can pick. You (the caller) get to choose exactly what type you
give me.
The
In Haskell, I sometimes have to annotate code with type info because the
type-inferer otherwise fails (even with |-XNoMonomorphismRestriction)|.
Surely, most of the time this is because I was writing buggy code, but
sometimes, type annotation just seems needed to get a successful
compilation
2008/5/18 Peter Verswyvelen [EMAIL PROTECTED]:
In Haskell, I sometimes have to annotate code with type info because the
type-inferer otherwise fails (even with -XNoMonomorphismRestriction).
Surely, most of the time this is because I was writing buggy code, but
sometimes, type annotation just
Luke Palmer wrote:
Do you have an example of code that required an annotation to compile?
There is some trickiness around functions like read that can demand
explicit type signatures. You also sometimes get this with numeric
literals, array types, etc.
On Sun, 2008-05-18 at 16:57 +, Luke Palmer wrote:
2008/5/18 Peter Verswyvelen [EMAIL PROTECTED]:
In Haskell, I sometimes have to annotate code with type info because the
type-inferer otherwise fails (even with -XNoMonomorphismRestriction).
Surely, most of the time this is because I was
Hello Derek,
Sunday, May 18, 2008, 9:10:38 PM, you wrote:
This is incorrect. There are two (other) situations where you need type
annotations in Haskell 98. One situation is when you use polymorphic
recursion, but that is pretty rare unless you are writing nested data
types
can you give
On Sun, 2008-05-18 at 21:16 +0400, Bulat Ziganshin wrote:
Hello Derek,
Sunday, May 18, 2008, 9:10:38 PM, you wrote:
This is incorrect. There are two (other) situations where you need type
annotations in Haskell 98. One situation is when you use polymorphic
recursion, but that is pretty
On 10/30/07, Felipe Lessa [EMAIL PROTECTED] wrote:
On 10/30/07, Tim Chevalier [EMAIL PROTECTED] wrote:
ppos = pi/len2; pi and len2 are both Ints, so dividing them gives you
an Int. To convert to a Double, write ppos = fromIntegral (pi/len2).
(Type :t fromIntegral in ghci to see what else
On Tue, 30 Oct 2007, noa wrote:
I have the following function:
theRemainder :: [String] - [String] - Double
theRemainder xs xt = sum( map additional (unique xs) )
where
additional x = poccur * (inf [ppos,pneg]) --inf takes [Double]
where
xsxt = zip
On 10/30/07, noa [EMAIL PROTECTED] wrote:
Hi!
I have the following function:
theRemainder :: [String] - [String] - Double
theRemainder xs xt = sum( map additional (unique xs) )
where
additional x = poccur * (inf [ppos,pneg]) --inf takes [Double]
where
On 10/30/07, Tim Chevalier [EMAIL PROTECTED] wrote:
ppos = pi/len2; pi and len2 are both Ints, so dividing them gives you
an Int. To convert to a Double, write ppos = fromIntegral (pi/len2).
(Type :t fromIntegral in ghci to see what else fromIntegral can be
used for.)
You mean pi /
Hi!
I have the following function:
theRemainder :: [String] - [String] - Double
theRemainder xs xt = sum( map additional (unique xs) )
where
additional x = poccur * (inf [ppos,pneg]) --inf takes [Double]
where
xsxt = zip xs xt
pi =
On 10/30/07, Tim Chevalier [EMAIL PROTECTED] wrote:
On 10/30/07, noa [EMAIL PROTECTED] wrote:
Hi!
I have the following function:
theRemainder :: [String] - [String] - Double
theRemainder xs xt = sum( map additional (unique xs) )
where
additional x = poccur * (inf
The following code has ambiguity, but I can't figure out how to get
around it. Am I missing something trivial? Am I going in the wrong
direction? Thank you in advance for your time and for any help that
you can offer.
data MehQueue = MehQueue
class MehBase a where new :: IO a
instance
On 4/16/07, Paul Wankadia [EMAIL PROTECTED] wrote:
The following code has ambiguity, but I can't figure out how to get
around it. Am I missing something trivial? Am I going in the wrong
direction? Thank you in advance for your time and for any help that
you can offer.
How about changing
x
Felipe Almeida Lessa [EMAIL PROTECTED] wrote:
How about changing
x - new
to
x - new :: IO MehQueue
?
Is it impossible for the compiler to infer the type from the methods called?
(-fweird-strange-sick-twisted-eerie-godless-evil-stuff!-and-i-want-in.)
On 16/04/07, Paul Wankadia [EMAIL PROTECTED] wrote:
Is it impossible for the compiler to infer the type from the methods called?
Your code:
main :: IO ()
main = do
x - new
From the use of 'new', the compiler can infer that the type of x is an
instance of MehBase, and...
Hi. I have a type inference related problem which causes me some confusion. The following is a simplified example capturing the key aspects. First of all, consider a data type (here called) Elem and a type class IsElem.
data Elem = Eclass IsElem a where toElem :: a - Eleminstance IsElem Elem
Cale Gibbard wrote:
On 09/02/06, Brian Hulley [EMAIL PROTECTED] wrote:
Brian Hulley wrote:
f :: forall m. (forall a. a-m a) - c - d - (m c, m d)
Of course this type doesn't work on your original example, since (,)
is a type constructor with two parameters, not one, but this type
signature
Brian Hulley wrote:
Fred Hosch wrote:
Is type inferencing in Haskell essentially the same as in SML?
The most significant difference certainly is that type inference has
been beefed up with type classes in Haskell, which are quite a powerful
mechanism refining Hindley/Milner inference.
Is type inferencing in Haskell essentially the same as in SML? Thanks.
---Fred Hosch
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Fred Hosch wrote:
Is type inferencing in Haskell essentially the same as in SML? Thanks.
Well, that depends on what you mean by essentially the same ;-)
Both languages are based on the same Hindley-Milner type inference
algorithm, so both suffer from the same problem that a function such as
On 08/02/06, Brian Hulley [EMAIL PROTECTED] wrote:
Fred Hosch wrote:
Is type inferencing in Haskell essentially the same as in SML? Thanks.
Well, that depends on what you mean by essentially the same ;-)
Both languages are based on the same Hindley-Milner type inference
algorithm, so both
Cale Gibbard wrote:
On 08/02/06, Brian Hulley [EMAIL PROTECTED] wrote:
Fred Hosch wrote:
Is type inferencing in Haskell essentially the same as in SML?
Thanks.
Well, that depends on what you mean by essentially the same ;-)
Both languages are based on the same Hindley-Milner type inference
Brian Hulley wrote:
f :: (forall a m. a - m a) - c - d - (m c, m d)
The above is wrong - there is no way to quantify m properly. This must be
why intersection types need to be written with after all
___
Haskell-Cafe mailing list
Brian Hulley wrote:
Brian Hulley wrote:
f :: (forall a m. a - m a) - c - d - (m c, m d)
The above is wrong - there is no way to quantify m properly. This
must be why intersection types need to be written with after
all
What am I saying! It's right after all, and might be
Brian Hulley wrote:
Brian Hulley wrote:
Brian Hulley wrote:
f :: (forall a m. a - m a) - c - d - (m c, m d)
The above is wrong - there is no way to quantify m properly. This
must be why intersection types need to be written with after
all
What am I saying! It's right after
On 09/02/06, Brian Hulley [EMAIL PROTECTED] wrote:
Brian Hulley wrote:
Brian Hulley wrote:
Brian Hulley wrote:
f :: (forall a m. a - m a) - c - d - (m c, m d)
The above is wrong - there is no way to quantify m properly. This
must be why intersection types need to be written
Hi everyone,
I'm relatively new to Haskell and was a bit troubled by the problem
of assigning a type to infinite structures. To give a clear example,
suppose we have
data Nat = Zero | Succ Nat
omega = Succ omega
What type then does omega have? According to GHCi, omega :: Nat. But
surely
On 12/23/05, Matt Collins [EMAIL PROTECTED] wrote:
Hi everyone,
I'm relatively new to Haskell and was a bit troubled by the problem
of assigning a type to infinite structures. To give a clear example,
suppose we have
data Nat = Zero | Succ Nat
omega = Succ omega
What type then does omega
Thanks Sebastian, I guess I was ignoring the type of Succ like you
said. Glad to have passed that mental barrier!
On 23/12/2005, at 12:14 PM, Sebastian Sylvan wrote:
On 12/23/05, Matt Collins [EMAIL PROTECTED] wrote:
Hi everyone,
I'm relatively new to Haskell and was a bit troubled by the
Hi All,
I have been developing a type inference system which is very similar to type
classes' (by Wadler and Blott). However, I cannot find a detailed
description of the algorithm. In Type Classes in Haskell, implementation
issues are discussed briefly. However, it is too brief for me to
robert wong writes (in the Haskell Cafe):
I have been developing a type inference system which is very similar to
type classes' (by Wadler and Blott). However, I cannot find a detailed
description of the algorithm. In Type Classes in Haskell,
implementation issues are discussed briefly.
Malcolm Wallace wrote:
Christian Maeder [EMAIL PROTECTED] writes:
voidcast v@(VariantWithOne{}) = v { field1 = Void , field2 = Void }
Setting field2 only assures type correctness, but the value of field2
would be ignored at runtime.
Exactly what I was proposing.
I know, but how save is
Christian Maeder wrote:
Malcolm Wallace wrote:
Christian Maeder [EMAIL PROTECTED] writes:
voidcast v@(VariantWithOne{}) = v { field1 = Void , field2 = Void }
Setting field2 only assures type correctness, but the value of field2
would be ignored at runtime.
Exactly what I was proposing.
I
Malcolm Wallace wrote:
Yes, I find it interesting that consecutive updates are not equivalent
to a combined update. I believe this is largely because named fields
are defined as sugar - they behave in some sense like textual macros
in other languages, which can often turn out to have
Malcolm Wallace wrote:
I believe this is a very different question from the consecutive
update one.
I agree, consecutive and parallel updates are quite different.
I can see no
reason to outlaw a type change, where all the relevant types change
at the same time:
update_ok v@(A{}) = v
Christian Maeder [EMAIL PROTECTED] writes:
Typing fails in your original example:
voidcast [EMAIL PROTECTED] = v {field1 = Void}
but not in the lambda equivalent
voidcast [EMAIL PROTECTED] =
(\ (VariantWithOne a) - VariantWithOne Void) v
Hmm. Yes, that was my original point.
On Mon, 27 Jun 2005, Malcolm Wallace wrote:
I can only repeat myself, that the field being updated (and
type-converted) is only one of many, and all other fields should
carry the same value in the updated structure as in the original.
There is no good way to write this at the moment. If
Lennart Augustsson [EMAIL PROTECTED] wrote:
snip
There are, of course, type systems where my program works fine.
O'Haskell is an example of a language with such a type system. In
O'Haskell the Either type is defined like this:
data Left a = Left a
data Right a = Right a
Daniel Brown [EMAIL PROTECTED] wrote:
Jonathan Cast wrote:
Lennart Augustsson [EMAIL PROTECTED] wrote:
foo :: Either a b - Either () b
foo (Left _) = Left ()
foo x@(Right _) = x
Since Haskell type checking doesn't use the information gained by
pattern matching to refine types we
Tomasz Zielonka wrote:
voidcast v@(VariantWithTwo{}) = v { field1 = Void , field2 = Void }
voidcast v@(VariantWithOne{}) = v { field1 = Void }
I would not expect that updating only field1 can change the type of v.
But it can. Note that if you change the second field1 to field3 (both in
Lennart Augustsson [EMAIL PROTECTED] writes:
A somewhat similar problem exists even without fields:
foo :: Either a b - Either () b
foo (Left _) = Left ()
foo x@(Right _) = x
Your example is less surprising than mine with fields. The expression
x
on the rhs of the last clause has type
Malcolm Wallace wrote:
Whereas in the named field example, the rhs expression
v {field1=Void}
does indeed have the type
Fields Void
as declared in the signature. The expression explicitly converts all
the relevant interior fields to Void. At least, that is how it could
appear to a
Christian Maeder [EMAIL PROTECTED] writes:
voidcast :: Fields a - Fields Void
voidcast v@(VariantWithTwo{}) = v { field1 = Void , field2 = Void }
voidcast v@(VariantWithOne{}) = v { field1 = Void }
I would not expect that updating only field1 can change the type of v.
The right thing is to
Malcolm Wallace wrote:
Ah, but the reason I want to use field update, rather than a new
construction on the rhs, is that my type really has lots of other
fields (not mentioned here), which are all of fixed definite types
(not parametric). It is much nicer to be able to write
v { field1
Malcolm Wallace wrote:
Here is a strawman proposal, which does not fix the consecutive update
problem, but which might address the original typing problem.
I think it does not really address the original typing problem.
It would allow you to write:
voidcast v@(VariantWithTwo{}) = v { field1
Christian Maeder [EMAIL PROTECTED] writes:
voidcast v@(VariantWithOne{}) = v { field1 = Void , field2 = Void }
Setting field2 only assures type correctness, but the value of field2
would be ignored at runtime.
Exactly what I was proposing.
I could write a single expression that updated
Jonathan Cast wrote:
No type theory (that I know of) goes beyond System F in accepting
anything like foo. So, given the current state of the art, foo is
unconditionally ill-typed. That could change if someone comes up with a
/consistent/ type theory that accepts foo, but foo is
I have discovered something I believe to be a problem in Haskell'98,
although it is not a simple bug as such - it has more of the flavour of
an unintended mismatch in the interaction of two separate features.
Since Haskell is deeply principled language, a feature conflict is
extremely rare, and so
A somewhat similar problem exists even without fields:
foo :: Either a b - Either () b
foo (Left _) = Left ()
foo x@(Right _) = x
Since Haskell type checking doesn't use the information gained
by pattern matching to refine types we just have to accept that
some perfectly safe programs don't
I was under the impression that, in ghc 6.4 at least, GADTs did just that: use information gained by matching on the
type constructor to refine types. I sort-of expected that the extension to pattern matching would follow.
Or is that a nice paper waiting to be written?
Jacques
Lennart
On Thu, 23 Jun 2005, Lennart Augustsson wrote:
A somewhat similar problem exists even without fields:
foo :: Either a b - Either () b
foo (Left _) = Left ()
foo x@(Right _) = x
Since Haskell type checking doesn't use the information gained
by pattern matching to refine types we just have
On Thu, 23 Jun 2005, Malcolm Wallace wrote:
module Fieldbug where
data Fields a =
VariantWithTwo { field1 :: a
, field2 :: a }
| VariantWithOne { field1 :: a }
The key point here is that the data structure with named fields has more
than one constructor, and
Malcolm Wallace wrote:
voidcast :: Fields a - Fields Void
voidcast v@(VariantWithTwo{}) = v { field1 = Void , field2 = Void }
voidcast v@(VariantWithOne{}) = v { field1 = Void }
I would not expect that updating only field1 can change the type of v.
The right thing is to construct a new value.
On Thu, 23 Jun 2005, Christian Maeder wrote:
Malcolm Wallace wrote:
voidcast :: Fields a - Fields Void
voidcast v@(VariantWithTwo{}) = v { field1 = Void , field2 = Void }
voidcast v@(VariantWithOne{}) = v { field1 = Void }
I would not expect that updating only field1 can change the type of
Lennart Augustsson [EMAIL PROTECTED] wrote:
A somewhat similar problem exists even without fields:
foo :: Either a b - Either () b
foo (Left _) = Left ()
foo x@(Right _) = x
Since Haskell type checking doesn't use the information gained
by pattern matching to refine types we just have to
On Thu, Jun 23, 2005 at 09:08:12PM +0200, Christian Maeder wrote:
Malcolm Wallace wrote:
voidcast :: Fields a - Fields Void
voidcast v@(VariantWithTwo{}) = v { field1 = Void , field2 = Void }
voidcast v@(VariantWithOne{}) = v { field1 = Void }
I would not expect that updating only field1
It's true that GADTs does just that. But only if you use them.
And they are not part of Haskell. :)
-- Lennart
Jacques Carette wrote:
I was under the impression that, in ghc 6.4 at least, GADTs did just
that: use information gained by matching on the type constructor to
refine types.
Jonathan Cast wrote:
Lennart Augustsson [EMAIL PROTECTED] wrote:
A somewhat similar problem exists even without fields:
foo :: Either a b - Either () b
foo (Left _) = Left ()
foo x@(Right _) = x
Since Haskell type checking doesn't use the information gained
by pattern matching to refine
76 matches
Mail list logo
