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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
