Re: type aliases and Id
A very good point. But that just makes a design that could include Id even more intriguing. :) -- Lennart On Mar 22, 2007, at 01:21 , [EMAIL PROTECTED] wrote: Lennart Augustsson wrote: 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. I wonder if this proposal is a good idea. Let us consider the following near-Haskell98 code class C a instance C (m a) instance C Int (usually there will be constraints on m. We shall see a useful example of this in a moment). This code typechecks under slight and common relaxation of the rules on the form of instance head. That example will probably typecheck in Haskell'. Under the proposal that Id t === t, typechecking of this code will require overlapping instances, which quite unlikely to make it into Haskell' and is a quite significant and controversial extension. Speaking of overlapping instances, let's generalize the example to class C a instance C (m a) instance C a It does typecheck in current Haskell. Under the Id proposal, this example will NOT typecheck, ever. This is because the two instances become exact duplicates. Indeed, every type that matches "a" will match "m a" (with m = Id) and vice versa. The two instances match the same class of types (that is, all of the types). Let us come back to our simple example and make it practical. class C a where incr :: a -> a instance (C a, Functor m) => C (m a) where incr = fmap incr instance C Int where incr = succ test = incr (Just [[[1::Int]]]) the example increments integers deeply embedded in some functorial data structures. The operations of this kind are requested from time to time on Haskell-Cafe. This code compiles and works (no overlapping or undecidable instances are required). Under the Id t === t proposal, this example will diverge (perhaps, it will diverge even in the compiler). The reason is that the base case cannot be reached; the type Int can always be considered as Id Int and so the first instance will apply again. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
type aliases and Id
Lennart Augustsson wrote: > 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. I wonder if this proposal is a good idea. Let us consider the following near-Haskell98 code > class C a > instance C (m a) > instance C Int (usually there will be constraints on m. We shall see a useful example of this in a moment). This code typechecks under slight and common relaxation of the rules on the form of instance head. That example will probably typecheck in Haskell'. Under the proposal that Id t === t, typechecking of this code will require overlapping instances, which quite unlikely to make it into Haskell' and is a quite significant and controversial extension. Speaking of overlapping instances, let's generalize the example to > class C a > instance C (m a) > instance C a It does typecheck in current Haskell. Under the Id proposal, this example will NOT typecheck, ever. This is because the two instances become exact duplicates. Indeed, every type that matches "a" will match "m a" (with m = Id) and vice versa. The two instances match the same class of types (that is, all of the types). Let us come back to our simple example and make it practical. > class C a where incr :: a -> a > > instance (C a, Functor m) => C (m a) where incr = fmap incr > instance C Int where incr = succ > > test = incr (Just [[[1::Int]]]) the example increments integers deeply embedded in some functorial data structures. The operations of this kind are requested from time to time on Haskell-Cafe. This code compiles and works (no overlapping or undecidable instances are required). Under the Id t === t proposal, this example will diverge (perhaps, it will diverge even in the compiler). The reason is that the base case cannot be reached; the type Int can always be considered as Id Int and so the first instance will apply again. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: type aliases and Id
| 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 still don't know how to do inference. Consider f :: forall m a. m a -> a -> [a] t :: Tree Int and consider the call f t t Well, this is perfectly well typed thus (I'll add the type applications to make it totally clear): f Id (Tree Int) t t That is, instantiate m=Id, a=Tree Int, and voila. The trouble is, when unifying (m a) = (Tree Int), it's very unclear what to do. Hmm. I suppose you might defer such unifications, instead gathering them as constraints, and solving them only when you quantify. That's the standard way to deal with tricky unification problems. It's certainly a nice challenge. Simon | | Perhaps a good topic for a research paper? | | -- Lennart | | On Mar 20, 2007, at 12:00 , Simon Peyton-Jones wrote: | | > | 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 problems? My gut feeling is that with just Id, you | > | probably don't, but I would not bet on it. | > | | > | Having Id would be cool. If we make an instance 'Monad Id' it's now | > | possible to get rid of map and always use mapM instead. Similarly | > | with other monadic functions. | > | > I remember that I have, more than once, devoted an hour or two to | > the question "could one add Id as a distinguished type constructor | > to Haskell". Sadly, each time I concluded "no". | > | > I'm prepared to be proved wrong. But here's the difficulty. | > Suppose we want to unify | > (m a) with (Tree Int) | > | > At the moment there's no problem: m=Tree, a=Int. But with Id | > another solution is | > m=Id, a=Tree Int | > | > And there are more | > m=Id, a=Id (Tree Int) | > | > We don't know which one to use until we see all the *other* uses of | > 'm' and 'a'. | > | > I have no clue how to solve this problem. Maybe someone else | > does. I agree that Id alone would be Jolly Useful, even without | > full type-level lambdas. | > | > Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: type aliases and Id
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. Perhaps a good topic for a research paper? -- Lennart On Mar 20, 2007, at 12:00 , Simon Peyton-Jones wrote: | 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 problems? My gut feeling is that with just Id, you | probably don't, but I would not bet on it. | | Having Id would be cool. If we make an instance 'Monad Id' it's now | possible to get rid of map and always use mapM instead. Similarly | with other monadic functions. I remember that I have, more than once, devoted an hour or two to the question "could one add Id as a distinguished type constructor to Haskell". Sadly, each time I concluded "no". I'm prepared to be proved wrong. But here's the difficulty. Suppose we want to unify (m a) with (Tree Int) At the moment there's no problem: m=Tree, a=Int. But with Id another solution is m=Id, a=Tree Int And there are more m=Id, a=Id (Tree Int) We don't know which one to use until we see all the *other* uses of 'm' and 'a'. I have no clue how to solve this problem. Maybe someone else does. I agree that Id alone would be Jolly Useful, even without full type-level lambdas. Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: type aliases and Id
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? All I did is add an expansion rule for my Id constructor to the place where the SizeOf pseudo-constructor was expanded. This basically means that if the typechecker sees Id applied so something, it is simplified out (as part of type-normalization / synonym expansion). 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 problems? My gut feeling is that with just Id, you probably don't, but I would not bet on it. I didn't change the unification rules, so 'm a', would NOT unify with 'a' with m=Id. That was mainly because I didn't need that unification rule to handle the case where I used the Id constructor. Having Id would be cool. If we make an instance 'Monad Id' it's now possible to get rid of map and always use mapM instead. Similarly with other monadic functions. Did you do that in the Bluespec compiler? I did experiment with Monad Id while trying to sort something else out, and it seemed to work (the instance typechecked as well as some code that depended on that instance), but I didn't push it very hard. Beyond that, in response to your note, I tried to see what would happen if I added a unification rule for 'm a' with 'a', with m=Id. There turned out to be three important details (to keep existing Bluespec code working): - make sure to choose to unify 'm a' with a separate type variable 'b' directly, in preference to setting m=Id and unifying a with b. Upon reflection, that seemed reasonable because it didn't prevent setting m=Id later, in response to additional information. - make sure not to replace m with Id, if m is a lexically-bound type variable - make sure to expand type synonyms before attempting this sort of unification After that I could typecheck simple things like the following (using an inferred identity monad): x :: Integer x = return 5 y :: List Integer y = mapM (const 5) (cons 1 (cons 2 nil)) However, I did run into the problems Iavor and Simon mentioned. For example, the following program did not typecheck: z :: Bool -> Maybe (Integer) z p1 = let f a0 b0 = let a = return a0 b = return b0 in if p1 then a else b in f 5 (Just 6) However, the same could *would* typecheck if I added the following type annotations: z :: Bool -> Maybe (Integer) z p1 = let f a0 b0 = let a = return (a0 :: Integer) b = return (b0 :: Maybe Integer) in if p1 then a else b in f 5 (Just 6) So, I'd say the results were intriguing but not terribly satisfying. My guess is many common uses would work out, but there would be hard-to-explain corner cases where the typechecker would need guidance or a desired level of polymorphism couldn't be achieved. - Ravi ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: type aliases and Id
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. The solutions are: 0: Int, Tree 1: Tree Int, Id 2: Id (Tree Int), Id 3: Id (Id (Tree Int)), Id Let [EMAIL PROTECTED] denote n-ary type-level application, where T is a list of types, and i>=0. Consider the pair ( S!!(i+1), (take i S)@i) This is the /closed-form/ for the n'th solution (m, a) for unifying (m a) with (Tree Int). A better way to _represent_ this closed form is as (S, i) where S = [Int,Tree, Id, Id, ...] from which further constraints can decide what is the 'proper' value of i to take. This even shows how to do defaulting: in the absence of further information, take the smallest i possible. [I phrase it this way because there are times where constraints will force a certain minimum on i, but no maximum]. In other words, the above should be backwards compatible with current behaviour, since the 'default' solution would be m=Tree, a=Int. Jacques Simon Peyton-Jones wrote: I remember that I have, more than once, devoted an hour or two to the question "could one add Id as a distinguished type constructor to Haskell". Sadly, each time I concluded "no". I'm prepared to be proved wrong. But here's the difficulty. Suppose we want to unify (m a) with (Tree Int) At the moment there's no problem: m=Tree, a=Int. But with Id another solution is m=Id, a=Tree Int And there are more m=Id, a=Id (Tree Int) We don't know which one to use until we see all the *other* uses of 'm' and 'a'. I have no clue how to solve this problem. Maybe someone else does. I agree that Id alone would be Jolly Useful, even without full type-level lambdas. Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: type aliases and Id
| 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 problems? My gut feeling is that with just Id, you | probably don't, but I would not bet on it. | | Having Id would be cool. If we make an instance 'Monad Id' it's now | possible to get rid of map and always use mapM instead. Similarly | with other monadic functions. I remember that I have, more than once, devoted an hour or two to the question "could one add Id as a distinguished type constructor to Haskell". Sadly, each time I concluded "no". I'm prepared to be proved wrong. But here's the difficulty. Suppose we want to unify (m a) with (Tree Int) At the moment there's no problem: m=Tree, a=Int. But with Id another solution is m=Id, a=Tree Int And there are more m=Id, a=Id (Tree Int) We don't know which one to use until we see all the *other* uses of 'm' and 'a'. I have no clue how to solve this problem. Maybe someone else does. I agree that Id alone would be Jolly Useful, even without full type-level lambdas. Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: type aliases and Id
On Mon, Mar 19, 2007 at 07:55:30PM +, Lennart Augustsson wrote: > 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 problems? My gut feeling is that with just Id, you > probably don't, but I would not bet on it. I have actually very much wanted this on a couple occasions. the main one being the 'annotation problem'. an abstract syntax tree you might want to annotate with different types of data. the current solution is something like data Ef f = EAp (f E) (f E) | ELam Var (f E) newtype Identity x = Identity x -- annotate with nothing type E = Ef Identity -- annotate with free variables type EFV = Ef ((,) (Set.Set Var)) etc... unfortunately, it makes the base case, when there are no annotations, very verbose. if we had (Id :: * -> *) then we could make type E = Ef Id and just pretend the annotations arn't there. > Having Id would be cool. If we make an instance 'Monad Id' it's now > possible to get rid of map and always use mapM instead. Similarly > with other monadic functions. > Did you do that in the Bluespec compiler? I don't see how declaring instances for such a type synonym would be possible. Type synonyms are fully expanded before any type checking. (they are basically just type-level macros). An unapplied 'Id' would not be able to expand to anything, so you would not be able to create an instance for it. This is a little odd in that the instance is properly kinded, yet still invalid. but I don't see that as a big issue, as there are other reasons instances can be invalid besides being improperly kinded John -- John Meacham - ⑆repetae.net⑆john⑈ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: type aliases and Id
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. Do you know if you can run into higher order unification problems? My gut feeling is that with just Id, you probably don't, but I would not bet on it. It seems to me that even with just ''Id'' the problem is tricky. Suppose, for example, that we need to solve ''f x = g y''. In the present system we can reduce this to ''f = g'' and ''x = y'''. However, if we had ''Id'', then we would have to delay this equation until we know more about the variables that are involved (e.g., the correct solution might be ''f = Id'' and ''x = g y''). -Iavor ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: type aliases and Id
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. Do you know if you can run into higher order unification problems? My gut feeling is that with just Id, you probably don't, but I would not bet on it. Having Id would be cool. If we make an instance 'Monad Id' it's now possible to get rid of map and always use mapM instead. Similarly with other monadic functions. Did you do that in the Bluespec compiler? -- Lennart On Mar 19, 2007, at 19:26 , Ravi Nanavati wrote: 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 eta-reduce all type synonyms as much as possible, e.g. type T a b c d = X a b Int c d is equivalent to type T a b = X a b Int and type Id a = a is equivalent to a type that cannot be expressed directly. Any opinions? A third possibility is to have "Id" be a special primitive type constructor of kind * -> * that implementations handle internally. If you wanted to give it different name you could use an eta- reduced type synonym for that, of course. That's the approach I took when I needed an identity type function in the Bluespec compiler, and that worked out reasonably well. Part of the reason that worked out, though, is that we already had a normalization point during typechecking where certain special type constructors (related to numeric types) were cleaned out, so adding Id just extended that a little. I don't know whether adding such a constructor would be an equally simple change for Haskell implementations. And there's the separate argument that requiring eta-reduction of all type synonyms might be an interesting new feature in its own right (since I think you can say other new things beyond type Id a = a). - Ravi ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: type aliases and Id
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 eta-reduce all type synonyms as much as possible, e.g. type T a b c d = X a b Int c d is equivalent to type T a b = X a b Int and type Id a = a is equivalent to a type that cannot be expressed directly. Any opinions? A third possibility is to have "Id" be a special primitive type constructor of kind * -> * that implementations handle internally. If you wanted to give it different name you could use an eta-reduced type synonym for that, of course. That's the approach I took when I needed an identity type function in the Bluespec compiler, and that worked out reasonably well. Part of the reason that worked out, though, is that we already had a normalization point during typechecking where certain special type constructors (related to numeric types) were cleaned out, so adding Id just extended that a little. I don't know whether adding such a constructor would be an equally simple change for Haskell implementations. And there's the separate argument that requiring eta-reduction of all type synonyms might be an interesting new feature in its own right (since I think you can say other new things beyond type Id a = a). - Ravi ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: type aliases and Id
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 a b c d = X a b Int c d is equivalent to type T a b = X a b Int and type Id a = a is equivalent to a type that cannot be expressed directly. I like this alternatie a bit better, but I can also see how it introduces a lot of potential confusing, especially for novice Haskell programmers. You write something and the compiler goes along with something else... Maybe this will serve as a source of inspiration: http:// portal.acm.org/citation.cfm?doid=581478.581496 [1]. Cheers, Stefan [1] Matthias Neubauer and Peter Thiemann. Type classes with more higher-order poly- morphism. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02), Pittsburgh, Pennsylvania, USA, October 4–-6, 2002, pages 179–-190. ACM Press, 2002. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
type aliases and Id
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 remove the Maybe type so I can lose all the now-redundant Just
constructors.
Well, suppose in actual fact I prefer the name "CanBe" to Maybe.
Then for the first part I want
type CanBe a = Maybe a
foo :: Foo CanBe
foo = ...
but of course this fails because CanBe is a non-fully-applied type
synonym in "foo :: Foo CanBe", and I can fix this by eta-reducing thus:
type CanBe = Maybe
foo :: Foo CanBe
foo = ...
Now for the second part I want
type Id a = a
foo' :: Foo Id
foo' = ...
but again Id is not fully applied. However, this time I cannot
eta-reduce it! "type Id =" is a parse error, as is "type Id".
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 eta-reduce all type synonyms as much as
possible, e.g.
type T a b c d = X a b Int c d
is equivalent to
type T a b = X a b Int
and
type Id a = a
is equivalent to a type that cannot be expressed directly.
Any opinions?
Thanks
Ian
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
