Types of partially instantiated polymorphic helper functions
Dear Cafe, This has got to be a trivial question, but I don't see a solution, nor could I find anything through searching: If I want to write a type declaration for the helper function g here, what do I write? f :: a -> [b] -> [(a,b)] f a bs = g bs where g :: ???? g [] = [] g (x:xs) = (a,x) : g xs Apologies if I'm wasting bandwidth with my ignorance. Todd Wilson
Dear Todd, On 24/11/2020 22:26, Todd Wilson wrote:
This has got to be a trivial question, but I don't see a solution, nor could I find anything through searching: If I want to write a type declaration for the helper function g here, what do I write?
f :: a -> [b] -> [(a,b)] f a bs = g bs where g :: ???? g [] = [] g (x:xs) = (a,x) : g xs
This has a disappointingly not-entirely-trivial answer: {-# LANGUAGE ExplicitForAll, ScopedTypeVariables #-} f :: forall a b . a -> [b] -> [(a,b)] f a bs = g bs where g :: [c] -> [(a, c)] g [] = [] g (x:xs) = (a,x) : g xs We need the type variable `a` in the type of `g` to be the same as the one bound in the type of `f`, but Haskell2010 doesn't have a way to express this. The ScopedTypeVariables extension, when used with an explicit forall, makes the type variables scope over type signatures in the body of the function. Hope this helps, Adam -- Adam Gundry, Haskell Consultant Well-Typed LLP, https://www.well-typed.com/ Registered in England & Wales, OC335890 118 Wymering Mansions, Wymering Road, London W9 2NF, England
I see, thanks! And I guess that if the type variable c in your type of g
were changed to b, it will still work, but now g would have a monomorphic
instead of polymorphic type. I hope the combination of keywords in my
subject line can serve to direct someone else with this problem to your
answer!
Todd Wilson
On Tue, Nov 24, 2020 at 2:37 PM Adam Gundry
Dear Todd,
On 24/11/2020 22:26, Todd Wilson wrote:
This has got to be a trivial question, but I don't see a solution, nor could I find anything through searching: If I want to write a type declaration for the helper function g here, what do I write?
f :: a -> [b] -> [(a,b)] f a bs = g bs where g :: ???? g [] = [] g (x:xs) = (a,x) : g xs
This has a disappointingly not-entirely-trivial answer:
{-# LANGUAGE ExplicitForAll, ScopedTypeVariables #-}
f :: forall a b . a -> [b] -> [(a,b)] f a bs = g bs where g :: [c] -> [(a, c)] g [] = [] g (x:xs) = (a,x) : g xs
We need the type variable `a` in the type of `g` to be the same as the one bound in the type of `f`, but Haskell2010 doesn't have a way to express this. The ScopedTypeVariables extension, when used with an explicit forall, makes the type variables scope over type signatures in the body of the function.
Hope this helps,
Adam
-- Adam Gundry, Haskell Consultant Well-Typed LLP, https://www.well-typed.com/
Registered in England & Wales, OC335890 118 Wymering Mansions, Wymering Road, London W9 2NF, England
On Tue, Nov 24, 2020 at 02:58:33PM -0800, Todd Wilson wrote:
I see, thanks! And I guess that if the type variable c in your type of g were changed to b, it will still work, but now g would have a monomorphic instead of polymorphic type.
Yes, exactly. I was not going to post my otherwise redundant answer, but since it in fact makes `g` monomorphic, here it is: The simplest thing (which you probably already know) is to not give `g` a type signature, and let GHC infer the type. But since you asked, one solution is: {-# LANGUAGE ScopedTypeVariables #-} f :: forall a b. a -> [b] -> [(a, b)] f a bs = g bs where g :: [b] -> [(a, b)] g [] = [] g (x:xs) = (a, x) : g xs You need scoped type variables becase the `a` in the return-type of `g` needs to be the *same* `a` as in the signature of `f`, and unlike `f` the function `g` is not polymorphic in `a`, so you need a mechanis to identify the two instances of the type variable, and that's where the `ScopedTypeVariables` pragma comes into play. Once you have `ScopedTypeVariables`, you also get (for free) `ExplicitForall`, and each new universally quanitified type variable now needs "forall" to bring it into scope. -- Viktor.
On Tue, 24 Nov 2020, Viktor Dukhovni wrote:
On Tue, Nov 24, 2020 at 02:58:33PM -0800, Todd Wilson wrote:
I see, thanks! And I guess that if the type variable c in your type of g were changed to b, it will still work, but now g would have a monomorphic instead of polymorphic type.
Yes, exactly. I was not going to post my otherwise redundant answer, but since it in fact makes `g` monomorphic, here it is:
The simplest thing (which you probably already know) is to not give `g` a type signature, and let GHC infer the type. But since you asked, one solution is:
{-# LANGUAGE ScopedTypeVariables #-}
f :: forall a b. a -> [b] -> [(a, b)] f a bs = g bs where g :: [b] -> [(a, b)] g [] = [] g (x:xs) = (a, x) : g xs
An alternative would be to let g be polymorphic but add 'a' as parameter: f a bs = g a bs where g :: a -> [b] -> [(a, b)] g = map ((,) a)
Thanks for the additional responses. For the record, in response to
On Tue, Nov 24, 2020 at 3:51 PM Henning Thielemann
An alternative would be to let g be polymorphic but add 'a' as parameter:
f a bs = g a bs where g :: a -> [b] -> [(a, b)] g = map ((,) a)
this is what I had been doing before -- adding variables that were in scope as additional arguments to recursive helper functions, even though they don't change during recursive calls -- just so that I could give type annotations to helper functions for the purposes of documentation, since I didn't see any other way. (Of course, my helper function here is a simple application of `map`, but I was choosing this minimal example to illustrate something that came up repeatedly in more complicated situations.) The use of `ScopedTypeVariables`, though, is a better solution for me, since it allows me to continue my annotation practice without having to change the code I would ordinarily write. FWIW, my audience is college students using Haskell to supplement non-PL classes, and the annotations, perhaps more than usual, help them understand the code. Since I've already discussed polymorphism and type variables by that point, the explicit `forall`s (and language pragmas) are a satisfyingly minimal and easily explainable intrusion. Todd Wilson
On Tue, Nov 24, 2020 at 02:26:03PM -0800, Todd Wilson wrote:
This has got to be a trivial question, but I don't see a solution, nor could I find anything through searching: If I want to write a type declaration for the helper function g here, what do I write?
f :: a -> [b] -> [(a,b)] f a bs = g bs where g :: ???? g [] = [] g (x:xs) = (a,x) : g xs
You probably want this: {-# LANGUAGE ScopedTypeVariables #-} f :: forall a b. a -> [b] -> [(a,b)] f a bs = g bs where g :: [b'] -> [(a, b')] g [] = [] g (x:xs) = (a,x) : g xs
participants (5)
-
Adam Gundry -
Henning Thielemann -
Todd Wilson -
Tom Ellis -
Viktor Dukhovni