More Haskell Blue Sky: Partial Type Annotations
I sometimes come across a situation when I only want to provide a _partial_ type annotation, perhaps because the full type has some variable unified with some variable in some other type annotation, or something. For instance: f :: forall a. [a] -> [a] -> [a] f x y = g x where g [] = y g (_:_) = x ...there doesn't seem to be a way of giving a type annotation for 'g'. Theoretically it's '[a] -> [a]', but where 'a' is the same as the 'a' in the type signature for 'f'. Under this proposal, unqualified type variables would be considered to be 'free' rather than implicitly forall-qualified. So for instance, any function could be given the partial type annotation 'a -> b'. For instance, all these annotations would be the same given this function: k :: a k :: a -> ba k :: a -> b -> a k :: forall b. a -> b -> a k :: forall a b. a -> b -> a k x y = x ...and these would both be the same, but different from the previous: k' :: Int -> ba k' :: forall b. Int -> b -> Int k' x y = x And so we could write this: f :: forall a. [a] -> [a] -> [a] f x y = g x where g :: [a] -> [a] -- partial annotation may be sufficient g [] = y g (_:_) = x I admit that's a bit of a change, and might break programs... In addition, it doesn't address the occasional need to tie type annotations together, something that has often made me add ugly dummy arguments used just for their type. -- Ashley Yakeley, Seattle WA
I actually have wanted a similar thing at times, the proposal I had in mind was a bit less drastic, simply allow '_' in type signatures which will unify with any arbitrary type. that way you can give any function the type f :: _ -> _ or if you just want to resstrict part of the type you could say f :: _ -> Int or something like that. This gives you most of what your proposal does but doesnt break existing programs. the main thing it doesnt allow would be stating that two types are equivalant, yet unconstrained otherwise. such as f :: a -> a for instance. note that i would love it if forall and exists were made explicit, but it is a bit late for that, at least without breaking things. John On Thu, Apr 11, 2002 at 04:11:12AM -0700, Ashley Yakeley wrote:
I sometimes come across a situation when I only want to provide a _partial_ type annotation, perhaps because the full type has some variable unified with some variable in some other type annotation, or something. For instance:
f :: forall a. [a] -> [a] -> [a] f x y = g x where g [] = y g (_:_) = x
...there doesn't seem to be a way of giving a type annotation for 'g'. Theoretically it's '[a] -> [a]', but where 'a' is the same as the 'a' in the type signature for 'f'.
Under this proposal, unqualified type variables would be considered to be 'free' rather than implicitly forall-qualified. So for instance, any function could be given the partial type annotation 'a -> b'. For instance, all these annotations would be the same given this function:
k :: a k :: a -> ba k :: a -> b -> a k :: forall b. a -> b -> a k :: forall a b. a -> b -> a
k x y = x
...and these would both be the same, but different from the previous:
k' :: Int -> ba k' :: forall b. Int -> b -> Int
k' x y = x
And so we could write this:
f :: forall a. [a] -> [a] -> [a] f x y = g x where g :: [a] -> [a] -- partial annotation may be sufficient g [] = y g (_:_) = x
I admit that's a bit of a change, and might break programs... In addition, it doesn't address the occasional need to tie type annotations together, something that has often made me add ugly dummy arguments used just for their type.
-- Ashley Yakeley, Seattle WA
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
-- --------------------------------------------------------------------------- John Meacham - California Institute of Technology, Alum. - john@repetae.net ---------------------------------------------------------------------------
Somewhere (either Algorithms: AFA, some paper, or the haskell report) I read that seq evaluates its first argument to head normal form. I remember posting on this message forum or haskell-cafe that it evaluates the first argument to weak head normal form. At the time, I thought I was right, THEN I read whatever I read (I just cannot find the reference! sorry!) I also know that sometimes shoot off my mouth, (or in this case, my fingers!). I want to get my facts right. I still am trying to write a document about strictness and haskell evaluation for those of us without research degrees ;-) Anyway. my only other source is foldoc. head normal form (HNF) A lambda expression is in head normal form if its top level is either a variable, a data value, a built-in function applied to too few arguments or a lambda abstraction whose body is not reducible. I.e. the top level is neither a redex nor a lambda abstraction with a reducible body. An expression in HNF may contain redexes in argument postions whereas a normal form may not. See also Weak head normal form. I shall not post WHNF def as it is rather large. search google for foldoc if you want it. But the key thing is this example: The term was coined by {Simon Peyton Jones} to make explicit the difference between {head normal form} (HNF) and what {graph reduction} systems produce in practice. A lambda abstraction with a reducible body, e.g. \ x . ((\ y . y+x) 2) is in WHNF but not HNF. so it looks if seq reduced to head normal form, above would be reduced to (\x . 2+y) seq (\x ->(\y->reverse y) [1..]) this would seem to reduce indefinately to get to head normal form. The haskell report says can be used to tell the difference between _|_ and (\x->_|_). I'm not sure how, unless the following is what is meant to be demonstrated. Prelude> seq (error "foo") False *** Exception: foo Prelude> seq (\x -> error "foo") False False So, I guess, my first real question is, Which of HNF or WHNF does seq reduce its first argument to? It still appears to be WHNF but maybe I'm confused about HNF. Any referal to a paper describing the differences between HNF and WHNF (yes, that includes yours Simon PJ!) would be appreciated. Actually, I really, really want that reference to at least read that bit about WHNF. However, I'd love any correction or verefication of my thinking process. Thanks, Jay Cox
On Thu, 11 Apr 2002, Jay Cox wrote:
I still am trying to write a document about strictness and haskell evaluation for those of us without research degrees ;-)
Just to say something quick. There are a few of you that actually responded when I was going to write what I then called "A strictness FAQ" I thought I would have it out in less than a month so I could then thank you whenever I made it available. I'm not quite happy enough with it to consider announcing a release for everybody. Anyway, thanks to those who replied, and thanks to the haskell community in general. <Toast> Jay Cox
Jay Cox wrote:
... so it looks if seq reduced to head normal form, above would be reduced to (\x . 2+y)
seq reduces its first argument to weak head normal form, as in: f = seq (const undefined) "good" g = seq undefined "bad" Main> f "good" (93 reductions, 148 cells) Main> g " Program error: {undefined} (12 reductions, 56 cells)
seq (\x ->(\y->reverse y) [1..]) this would seem to reduce indefinately to get to head normal form.
Here the argument is in WHNF but not in HNF. Supplied with a second argument, seq would return this: h = seq (\x ->(\y->reverse y) [1..]) "good" Main> h "good" (89 reductions, 124 cells)
The haskell report says can be used to tell the difference between _|_ and (\x->_|_). I'm not sure how, unless the following is what is meant to be demonstrated.
Prelude> seq (error "foo") False *** Exception: foo Prelude> seq (\x -> error "foo") False False
That is exactly the point. And it is a bit weird, because it would seem that for a function it would make no difference, whether it is _|_ or (\x->_|_), because all you can do operationally with a function (if seq is not present) is to apply it to some argument and both _|_ and (\x->_|_) would give back _|_ in this case. But since seq is present in Haskell 98 (and for good reason: efficiency), this intuition breaks down: _|_ ARE (\x->_|_) different. As the Haskell report states, this weakens Haskell's parametricity properties, making for example shortcut deforestation (foldr c n (build g) = g c n) wrong in the presence of seq: build:: (forall b . (a -> b -> b) -> b -> b) -> [a] build g = g (:) [] u :: [Int] u = foldr undefined [] (build seq) v :: [Int] v = seq undefined [] Main> u [] (20 reductions, 35 cells) Main> v Program error: {undefined} (10 reductions, 51 cells) Hope the above helped to understand seq better. Janis. -- Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de
participants (4)
-
Ashley Yakeley -
Janis Voigtlaender -
Jay Cox -
John Meacham