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 HEAD
As Robert Dockins said, it's not implemented, and it isn't clear how to implement it. At this point it's looking fairly likely that my PhD thesis will be on this very topic, so stay tuned. -- Ben