| I don't think you need to produce 'a=Id (Tree Int)' since that
| reduces to 'a=Tree Int'.
| In general, you don't have to produce Id applied to anything, which
| gives me some hope that it's possible to add Id and still have
| decidable (and complete) type deduction.
Yes, that's true. But I
| Ganesh and I were discussing today what would happen if one adds Id
| as a primitive type constructor. How much did you have to change the
| type checker? Presumably if you need to unify 'm a' with 'a' you now
| have to set m=Id. Do you know if you can run into higher order
| unification
There is a general solution, but it essentially involves polymorphism
a-la-Omega (or as in Coq's Calculus of Inductive Constructions).
The most general description of (Tree Int) is as the Stream
S = [Int, Tree, Id, Id, ...]
You are now attempting to pull-off exactly 2 terms from that Stream.
Hi all,
Suppose I have a datatype:
data Foo a = Foo {
int :: a Int,
char :: a Char
}
where I start off with (Foo Nothing Nothing) :: Foo Maybe, gradually
accumulate values until I have (Foo (Just 5) (Just 'c')), and then I
want to
Ian,
Mmm...
* Allow type Id = (I prefer this to type Id as I think we are more
likely to want to use the latter syntax for something else later
on).
Looks kind of funny; I'm not too thrilled.
* Implementations should eta-reduce all type synonyms as much as
possible, e.g.
type T
On 3/19/07, Ian Lynagh [EMAIL PROTECTED] wrote:
I'd really like to be able to define an eta-reduced Id; I see two
possibilities:
* Allow type Id = (I prefer this to type Id as I think we are more
likely to want to use the latter syntax for something else later on).
* Implementations should
Hello,
On 3/19/07, Lennart Augustsson [EMAIL PROTECTED] wrote:
Ravi,
Ganesh and I were discussing today what would happen if one adds Id
as a primitive type constructor. How much did you have to change the
type checker? Presumably if you need to unify 'm a' with 'a' you now
have to set m=Id.
