enough to provide their slides.
Best regards,
Frantisek Farka
On Wed, 15 Apr 2015 22:28:51 +0100
Frantisek Farka wrote:
>
> *
>
> WORKSHOP ON TYPE INFERENCE AND AUTOMATED PROVING
>
> Tuesday the 12th o
Hello everyone,
as the 12th of May is getting closer I would like to invite you
yet again for the Workshop on Type Inference and Automated Proving
at University of Dundee.
Please send me an email if you wish to attend as described bellow.
It helps us with organization.
For those who have not
On Thu, 16 Apr 2015 11:13:19 +0700
Kim-Ee Yeoh wrote:
Hi Kim-Ee,
I am afraid we currently do not plan to record the talks. But if
anything changes anf there will be any recordings I will send an email
to let the people in this mailing list know.
Best,
Franta
> Hi František,
>
> Do you think
*
WORKSHOP ON TYPE INFERENCE AND AUTOMATED PROVING
Tuesday the 12th of May, 12PM to 6PM
School Of Computing,
University of Dundee
http://staff.computing.dundee.ac.uk/frantisekfarka/tiap
m wrote:
>>
>> This is also available as html at
>>
>> http://repetae.net/computer/jhc/record_inference.html
>>
>> Record Type Inference
>> =
>>
>> An extension to the named field mechanism that will greatly enhance the
This is also available as html at
http://repetae.net/computer/jhc/record_inference.html
Record Type Inference
=
An extension to the named field mechanism that will greatly enhance the
utility of them when combined with the existing `DisambiguateRecordFields`,
`RecordPuns
t; this...
> http://hackage.haskell.org/trac/haskell-prime/wiki/NoMonomorphismRestriction
>
> But even with MonomorphismRestriction, issue 1/2 are avoidable with
> a more refined approach to type meta variables in the Haskell type
> inference: After type-checking a strongly connected co
Congratulations to all that solved the riddle so quickly. (First answer
in only 8 Minutes!) Now to the point of the exercise: Shocking
realizations.
1. Haskell's type inference is NON-COMPOSITIONAL!
In the riddle below, I am defining two things f ("rgbliste") and g
(&quo
Friends
Many of you will know that I've been muttering about re-engineering GHC's type
inference engine for some time now. Dimitrios, Tom, Martin and I have just
completed an epic paper describing the Glorious New Framework that forms the
substance of the above mutterings:
On Tue, 2009-01-27 at 10:05 -0800, Corey O'Connor wrote:
> On Tue, Jan 27, 2009 at 4:51 AM, wrote:
> > Doug McIlroy wrote:
> >> A fragment of an attempt to make pairs serve as complex numbers,
> >> using ghc/hugs extensions:
> >>
> >> instance Num a => Num (a,a) where
> >>
>>> (x,y) * (u,v) = (x*u-y*v, x*v+y*u)
>> The recent versions of GHC have a nifty equality constraint, so the
>> code can be written simply
>
> I'm confused on why
> instance Num a => Num (a, a) where
>
> is not equivalent to
> in
u)
> The recent versions of GHC have a nifty equality constraint, so the
> code can be written simply
I'm confused on why
instance Num a => Num (a, a) where
is not equivalent to
instance (Num a, Num b, a ~ b) => Num (a, b) where
I don't know the details of the type inferen
In ghc 6.10.1 the ~ constraint is working:
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
module D where
instance (Num a, Num b, a ~ b) => Num (a,b) where
(x,y) * (u,v) = (x*u-y*v, x*v+y*u)
test1 = (1,1) * (2,2)
test2 = (1,1.0)
Doug McIlroy wrote:
> A fragment of an attempt to make pairs serve as complex numbers,
> using ghc/hugs extensions:
>
> instance Num a => Num (a,a) where
> (x,y) * (u,v) = (x*u-y*v, x*v+y*u)
>
> Unfortunately, type inference isn'
Lennart Augustsson wrote:
>> I had hoped that the code below (GHC 6.10+) would work, but it just
>> sends GHC into a loop when you actually try to typecheck (1,1). I
>> don't know if that's a bug in GHC or a misunderstanding on my part of
>> how the typechecking should work.
> A loop without turn
instance Num a => Num (a,a) where
>> (x,y) * (u,v) = (x*u-y*v, x*v+y*u)
>>
>> Unfortunately, type inference isn't strong enough to cope with
>>
>> (1,1)*(1,1)
>>
>> Why shouldn't it be strengthened to do so?
>
>
Doug McIlroy wrote:
> A fragment of an attempt to make pairs serve as complex numbers,
> using ghc/hugs extensions:
>
> instance Num a => Num (a,a) where
> (x,y) * (u,v) = (x*u-y*v, x*v+y*u)
>
> Unfortunately, type inference isn'
Doug McIlroy wrote:
> instance Num a => Num (a,a) where
> (x,y) * (u,v) = (x*u-y*v, x*v+y*u)
>
> Unfortunately, type inference isn't strong enough to cope with
>
> (1,1)*(1,1)
I'm guessing it is because
(fromInteger 1,
A fragment of an attempt to make pairs serve as complex numbers,
using ghc/hugs extensions:
instance Num a => Num (a,a) where
(x,y) * (u,v) = (x*u-y*v, x*v+y*u)
Unfortunately, type inference isn't strong enough to cope with
(1,1)*(1,1)
Why shouldn
:).
Basically, the deal is that I have a language for which I need type
inference. I currently have something hacked together which works "most
of the time", but I'd really like to do it right. The problem is that
the type system is unlike anything I've encountered before.
jhc does it via the simple unification type inference algorithm,
modified to push explicitly given kinds down into terms. so, pretty much
exactly the boxy type inference algorithm, where your kind inference
function looks somewhat like
> data Kind =
> Star
> | Fun
Edsko,
Are there any papers that describe how higher kind type inference
(and I
really mean higher kind, not higher rank) is done?
I'm not aware of any specific papers (but maybe someone else can jump
in, here?), but as long as your kind language is simple enough, say
Hi,
Are there any papers that describe how higher kind type inference (and I
really mean higher kind, not higher rank) is done?
Thanks,
Edsko
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
On 7/7/06, Emil Axelsson <[EMAIL PROTECTED]> wrote:
Hello!
I'm observing a strange type inference result in the program at the end of the
message.
term1 and term2 have the same definitions, except for a type annotation for
term2, but GHCi infers the following types:
*Main>
Hello!
I'm observing a strange type inference result in the program at the end of the
message.
term1 and term2 have the same definitions, except for a type annotation for
term2, but GHCi infers the following types:
*Main> :t term1
term1 :: Term ()
*Main> :t term2
term2 :: foral
Again, you mean we cannot meaningfully annotate some lambda expression
so that the whole expression has this type and the annotation
"forall b. (a,b) -> (b,a)" be somehow fixed to its argument? Yes, this
is right, we have to use annot.
>
> Perhaps I am missing something here thou
Hi,
I am currently studying the paper "Practical Type Inference for
Arbitrary Rank Types" by Simon Peyton Jones and Mark Shields, and I've
been wondering about the final version of the typing rules (figure 7,
"Bidirectional version of Odersky-Laufer") (although I suppose
On Mon, Feb 27, 2006 at 04:42:32PM +0100, Johannes Waldmann wrote:
> Implicit parameters are *evil*. They seem to simplify programs
> but they make reasoning about them much harder.
Indeed. We really need some big caveats in the manual. I find a lot of
new users think they are what they need and j
Implicit parameters are *evil*. They seem to simplify programs
but they make reasoning about them much harder.
To an extent, they can be simulated with type classes,
because dictionaries are also implicit (you don't see them in the code
but you see them in the type declaration - same as for implic
Hi,
thanks for the last help and hints. I have encountered an other problem,
and again I don't quite understand the reason why I get the results I
get. ghci seems to infer different types for the same expression.
Consider that I have disabled the monomorphism restriction
in module AGC.lhs (which
>> > instance CpsForm t t where
>> This can't be right, can it?
> In general no: the CPS of a function certainly doesn't fit the above
> pattern. So, if the source language has abstractions (the language in
> the original message didn't), we have to add another instance for
> CpsForm.
But any othe
Stefan Monnier wrote:
> > instance CpsForm t t where
>
> This can't be right, can it?
In general no: the CPS of a function certainly doesn't fit the above
pattern. So, if the source language has abstractions (the language in
the original message didn't), we have to add another instance for
CpsFor
> instance CpsForm t t where
This can't be right, can it?
After CPS conversion a term of type "a -> b" won't have type "a -> b"
but rather something like "a * (b -> c) -> c".
Stefan
___
Haskell mailing list
Haskell@haskell.org
http://www.haske
2005 05:57
| To: haskell@haskell.org
| Subject: [Haskell] GADT type inference problem
|
|
| Let us consider the following simple code
|
| > {-# OPTIONS -fglasgow-exts #-}
| >
| > module Foo where
| >
| > data Term a where
| >B:: Bool -> Term Bool
| >C::
[EMAIL PROTECTED] writes:
>
> Let us consider the following simple code
>
> > {-# OPTIONS -fglasgow-exts #-}
> >
> > module Foo where
> >
> > data Term a where
> >B:: Bool -> Term Bool
> >C:: Term Bool -> Term t -> Term t
> >I:: Int -> Term Int
> >
> > shw (I t) = ("I "+
Let us consider the following simple code
> {-# OPTIONS -fglasgow-exts #-}
>
> module Foo where
>
> data Term a where
>B:: Bool -> Term Bool
>C:: Term Bool -> Term t -> Term t
>I:: Int -> Term Int
>
> shw (I t) = ("I "++) . shows t
> shw (B t) = ("B "++) . shows t
> shw (
Louis-Julien Guillemette wrote:
> Say we are using a GADT to represent a simple language of boolean
> constants and conditionals,
>
> data Term a where
>B:: Bool -> Term Bool
>Cnd :: Term Bool -> Term t -> Term t -> Term t
>
> and we would like to perform a type-safe CPS conversion ov
Louis-Julien Guillemette <[EMAIL PROTECTED]> wrote:
> Say we are using a GADT to represent a simple language of boolean
> constants and conditionals,
>
> data Term a where
>B:: Bool -> Term Bool
>Cnd :: Term Bool -> Term t -> Term t -> Term t
>
> and we would like to perfo
Say we are using a GADT to represent a simple language of boolean
constants and conditionals,
data Term a where
B:: Bool -> Term Bool
Cnd :: Term Bool -> Term t -> Term t -> Term t
and we would like to perform a type-safe CPS conversion over this language. We
encode the relationship
Thanks for the detailed explanation that helped clearing up the smog in
my head. I reckoned that once more the MR was to blame, at least for
part of it.
in particular, when I compare with the single parameter case:
class C a where fc :: a -> a -> ()
c1 x = let p = fc x in ()
c2 x = let p y
Hello,
On 4/25/05, Andrew Pimlott <[EMAIL PROTECTED]> wrote:
> I appreciated your explanation, but can you also address (to the list)
> the last case given by the original poster?
>
> > On 4/25/05, Andreas Rossberg <[EMAIL PROTECTED]> wrote:
> > > in particular, when I compare with the single par
Hello,
The type inference for "d1", goes on like this:
1. suppose "x" is of some type "a"
2. now lets infer a type for "p"
3. using the usual rules we infer that "p :: b -> ()",
subject to the constraint that "D a b" holds.
4. &q
This may well be stupidity on my side, but some experiments with multi
parameter type classes got me slightly confused. Can somebody explain
the following behaviour to me?
class D a b where fd :: a -> b -> ()
d1 x = let p = fd x in ()
d2 x = let p y = fd x y in ()
GHC derives the following
We would like to announce a technical report and a web-accessible
software demonstration.
The technical report is:
Type Inference and Principal Typings for
Symmetric Record Concatenation and Mixin Modules
by Henning Makholm and J. B. Wells
http://www.macs.hw.ac.uk/~makholm/papers
Hi
I did a Web application for the visualization of the type inference process for
the Simple Type System and pure ML. You can "play" with it at:
http://www.ncc.up.pt/typetool
I think it can be useful to Haskell programmers.
Comments are welcome,
Best regards
H
Hi
Question:
For what reason we need the "Type
inference" if we can enforce "Type constraints" ?
Thanks in
advance.
Dear all,
the following might be of interest to Haskellians and Types people.
I'd like to announce the availability of
TIE: A CHR-based Type Inference Engine
We present a generic type inference algorithm for Hindley/Milner style
systems based on Constraint Handling Rules (CHRs).
The s
Musing on Zhanyong's problem some more, a solution occurs to me.
Curiously, it's exactly the solution required for another useful
extension to type classes. Here is is, so people can shoot holes in it.
| In more detail, here's what happens. First we typecheck the RHS of
| f, deducing the types
| > My question is: how does the type inference algorithm work in the
| > presence of rank-2 types? Does anyone know of any documentation on
| > this? Thanks!
I had a look at this. Actually it turns out to be only loosely related
to rank-2 polymorphism. I've been able to
er a
*** Type : Sub b Int -> Super b _2
*** Given context : ()
*** Constraints : SubType (Sub b Int) (Super b _2)
Aha, this is something interesting! Either there is no standard for the
Haskell rank-2 type inference algorithm (which is a sad thing), or one
of hugs and ghc is wrong
eclaration for `SubType (Sub c
a) (Super
c Int)'
arising from use of `super' at R2Test.hs:16
In the right-hand side of a lambda abstraction: super a
If I remove the "forall c." from the type signature for f, then both
compilers accept my code.
My question is: how does t
Hi Keith,
| Type inference for Haskell (as described in Mark Jones' paper _Typing
| Haskell In Haskell_ and as performed by GHC) requires first splitting
| groups of let bindings into strongly-connected components. It then
| assumes that all binders in such a component will be genera
Type inference for Haskell (as described in Mark Jones' paper _Typing
Haskell In Haskell_ and as performed by GHC) requires first splitting
groups of let bindings into strongly-connected components. It then
assumes that all binders in such a component will be generalised over
the same v
At 10:48 am -0300 20/5/99, Carlos Camarao de Figueiredo wrote:
> investigate (it seems a little strange to provide type inference and
> also require top-level type declarations).
Well I might disagree - I'm one of those who think type declarations help to document
the code, thoug
On 24-Apr-1998, Frank A. Christoph <[EMAIL PROTECTED]> wrote:
> Does anyone know if Hindley-Milner type inference has been characterized in
> a non-operational way?
I've seen a lot of recent papers which talk about type inference
as constraint solving: the type system just
Does anyone know if Hindley-Milner type inference has been characterized in
a non-operational way? I mean either some sort of canonical correspondence
(as the simply typed lambda-calculus with intuitionistic natural deduction)
or some statement that describes it in terms of a universal property
Frank A. Christoph <[EMAIL PROTECTED]> writes:
> Does anyone know if Hindley-Milner type inference has been characterized in
> a non-operational way? I mean either some sort of canonical correspondence
> (as the simply typed lambda-calculus with intuitionistic natural deduct
Simon L Peyton Jones wrote:
>
> I think the report has it about right.
>
> * A conforming implementation of Haskell 1.4 must support mutually recursive
> modules. That is, a collection of individually legal mutually recursive
> modules is a legal Haskell program.
Well, this is not clear fr
| 5.4 Separate Compilation
|
|Depending on the Haskell implementation used, separate compilation of
|mutually recursive modules may require that imported modules contain
|additional information so that they may be referenced before they are
|compiled. Explicit type sign
> This isn't muddling implemenation with language design. The language design
> says mutual recursion is OK. A particular implementation supporting separate
> compilation will typically require a variety of "help", such as a Makefile
> with accurate dependencies. Requiring type signatures, or in
> I think the report has it about right.
>
> * A conforming implementation of Haskell 1.4 must support mutually recursive
> modules. That is, a collection of individually legal mutually recursive
> modules is a legal Haskell program.
>
> * The Report recognises that implementations availabl
| Why muddle implementation with language design? Pick a design that
| we know everyone can implement -- e.g., exported functions must have
| type declarations -- and stick to that. When the state of implementations
| improve, the specification for Haskell 1.5 can change accordingly. -- P
Act
Koen Claessen wrote:
> So, the Haskell compiler gives also an error here. I don't see the
> difference between "The class variable must occur in every method type"
> (Haskell) and "All the class variables must occur in every method type"
> (Gofer).
> The Gofer way is rejected, because it is amb
> Doesn't Haskell do the same if you say:
>
> class Cow a where
> pig :: a -> Int
> fly :: Int
This is not legal Haskell. The class variable must occur
in every method type.
-- Lennart
Lennart Augustsson wrote:
| > class Cow a where
| > pig :: a -> Int
| > fly :: Int
| This is not legal Haskell. The class variable must occur
| in every method type.
So, the Haskell compiler gives also an error here. I don't see the
difference between "The class variable must oc
On Thu, 24 Oct 1996, Benedict R. Gaster wrote:
| > class Sequence a s where
| > cons :: a -> s -> s
| > nth :: s -> Int -> a
| > len :: s -> Int
|
| > instance Sequence a (List a) where
| >
Hi,
Erik Meijer proposes that the Haskell type system be replaced by the Gofer
type system. In particular the Gofer type system does not require type
constraints to be of the form C a where C is a class identifier and a is
a type variable. Also maybe somewhat more motivating is the fact that Gof
Recently, Simon posted this message which describes a problem
that is caused by the fact that Haskell demands type constraints
to be of the form C a where C is a class identifier and a is a type
variable.
This is not the first time that people have complained about a problem of
this sort.
Since
This type error comes up such a lot that I'm copying this message
to the Haskell mailing list.
| The following program does not typecheck under ghc-2.01 unless you
| uncomment the type signature for test. (ghc-0.29 seems to propagate
| the equality attribute correctly, and doesn't require the a
In message <[EMAIL PROTECTED]:, S.D.Mechveliani writes:
:
: I tried to find out how Haskell understands the "lambda" programming.
: Here is the script for the length of a list.
: This is the so-called continuation passing stile, I believe.
:
: lng :: [a] -> Int
:
: lng = (\ xs ->
: (
I tried to find out how Haskell understands the "lambda" programming.
Here is the script for the length of a list.
This is the so-called continuation passing stile, I believe.
lng :: [a] -> Int
lng = (\ xs ->
( (\xs c -> if null xs then 0 else 1+(c (tail xs) c) )
xs
The Haskell type system is complicated and much of the complication
seems to result from supporting type inference.
Already we have a variety of situations where explicit type
signatures are required. For example:
1. Because of the monomorphism restriction, a type signatures is
modified occur-check). It is a "well-behaving"
undecidability.
You can modify an ordinary (unification-based) type-inference
algorithm as follows to get the more general types:
when type-checking a recursive definition, say
letrec f = ... f . f ...
use a fresh type va
Original-Via: uk.ac.nsf; Fri, 15 Nov 91 20:43:50 GMT
Has anyone looked at the complexity of type inference in Haskell
(similar to analogous results for ML)? Nipkow and Snelting have shown
how to reduce the inference problem to order-sorted unification (FPCA'91)
and they point out that
74 matches
Mail list logo
