weird (bug?) in linear implicit parameters

[Simon Peyton-Jones]

Yes, this is odd behaviour.  Here's what is is happening.
Consider

	foo :: %x::T =3D> Int -> [Int]
	foo 0 =3D []
	foo n =3D %x : foo (n-1)

where T is some type in class Splittable,

Do you get a list of all the same T's or all different T's?
(assuming that split gives two distinct T's back)

If you supply the type signature, taking advantage of polymorphic
recursion, you get what you'd probably expect.  Here's the
translated term, where the implicit param is made explicit:

	foo x 0 =3D []
	foo x n =3D let (x1,x2) =3D split x in=20
		   x1 : foo x2 (n-1)

But if you don't supply a type signature, GHC uses the Hindley
Milner trick of using a single monomorphic instance of the function
for the recursive calls. That is what makes Hindley Milner type
inference
work.  So the translation becomes

	foo x =3D let
			foom 0 =3D []
			foom n =3D x : foom (n-1)
		   in
		   foom

Result: 'x' is not split, and you get a list of identical T's.  That's
why
adding the type sig changes the behaviour.

You may say that this is a good reason to dislike linear implicit
parameters
and you'd be right.  That is why they are an experimental feature.
Unlike
many other features in GHC I am far from sure that it's a good one.

I'll dump this message into the user manual.

Simon

| -----Original Message-----
| From: Hal Daume III [mailto:hdaume@ISI.EDU]=20
| Sent: 23 July 2002 18:56
| To: GHC Users Mailing List
| Subject: weird (bug?) in linear implicit parameters
|=20
|=20
| (guess who finally decided to learn about imp params :P)
|=20
| this looks like a bug to me, but of course i may be wrong.
|=20
| consider these definitions:
|=20
| > data BLSupply =3D BLSupply [Bool]
| >=20
| > instance Splittable BLSupply where
| >     split (BLSupply l) =3D (BLSupply (True:l), BLSupply (False:l))
| >
| > newBL (BLSupply bl) =3D bl
|=20
| basically we can name things by lists of bools
|=20
| we name lists using this function:
|=20
| > number :: (%ns :: BLSupply) =3D> [a] -> [(a,[Bool])]
| > number [] =3D []
| > number (x:xs) =3D (x,n) : number xs
| >     where n =3D newBL %ns
|=20
| which works fine.  in ghci:
|=20
| *ImpParam> let %ns =3D BLSupply [] in number "hello"
| [('h',[False]),('e',[False,True]),('l',[False,True,True]),('l'
| ,[False,True,True,True]),('o',[False,True,True,True,True])]
|=20
| Whee.  now here's the wierd thing.  suppose we remove the=20
| type signature
| from the number function.  then, in ghci:
|=20
| *ImpParam> :t number
| forall a. (%ns :: BLSupply) =3D> [a] -> [(a, [Bool])]
| *ImpParam> let %ns =3D BLSupply [] in number "hello"
| [('h',[]),('e',[]),('l',[]),('l',[]),('o',[])]
|=20
| what gives?  why did it suddenly break even though it gets=20
| the type right?
|=20
|  - hal
|=20
| --
| Hal Daume III
|=20
|  "Computer science is no more about computers    | hdaume@isi.edu
|   than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume
|=20
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
|=20