Ben Rudiak-Gould Benjamin.Rudiak-Gould at cl.cam.ac.uk
Mon Feb 6 13:20:34 EST 2006

```Bulat Ziganshin wrote:
> Hello Ketil,
>
> KM> (Is the second ! actually meaningful?)
>
> yes! it means that the function is strict in its result - i.e. can't return
> undefined value when strict arguments are given.

Unfortunately this interpretation runs pretty quickly into theoretical
difficulties. A ! on the right hand side of a function arrow isn't like a !
on the left hand side. If you used this notation for this purpose, it would
have to be special-cased. Note that in GHC at present, a function of type
Int# -> Int# can diverge.

> KM>   foo :: [!a] -> ![a] -> a
>
> "![a]" means "strict list", it is
> the same as defining list with "next" field strict:
>
> data List2 a = Nil2 | List2 a !(List2 a)

This isn't consistent with the general rule that ! means absence of _|_. The
semantics that you want could be implemented as a special case for the []
constructor, but polymorphism breaks this, e.g.

data Foo a = MkFoo Int !a
data Bar a = MkFoo Int a
Foo [Bool] /= Bar ![Bool]

> for example, the following definition
>
> type Map a b = [(a,b)]
>
> will be instantiated to
>
> Map !Int String ==> [(!Int, String)]

As long as you're only specializing datatypes this works fine, but when you
try to do the same with polymorphic functions acting on those datatypes, you
run into serious problems. E.g.

f :: forall a. a -> Maybe a
f _ = Just undefined

Now we have (f :: Int -> Maybe Int) 3 == Just _|_, but (f :: !Int -> Maybe
!Int) 3 == _|_. This means that either f and all of its callers must be
specialized at compile time (despite having no type class constraints) or f
must inspect its implicit type argument at run time.

> such proposal already exists and supported by implementing this in GHC