On Sunday 19 October 2008 10:32:08 am Claus Reinke wrote:
(hint to ghc hackers: 'Data.Map.Map Int !Int' and '[!a]' would really be useful!-),
I can't figure out what that means though. Strictness is not a property of types or of values, it is a property of functions. [!] is not a subtype of [] ; IOW, there is no a such that [a] = [!Int] (where [!Int] is a list with strict values). For example, if we allowed this, the following property breaks:
length xs == length (map f xs)
Since it is not true on strict lists.
I'm not entirely sure this couldn't be worked out. Let's say that every type breaks into terminating and non-terminating computations:
a = !a | ^a
For your equation to break, you're assuming implicit conversions between some 'a' and '!a', ie, something like
(undefined :: a) :: !a (const undefined :: a -> b) :: !a -> !a
But those shouldn't typecheck! We can't decide termination, so not all objects of type 'a' can be classified into the subtypes '!a' or '^a'. Membership in '!a' can be constructive only, and map for strict lists would have a type somewhat like this
mapS :: !(!a -> !a) -> [!a] -> [!a]
Without a function, 'mapS' can't construct an element-strict result list, hence the first '!' (and 'mapS undefined' won't typecheck). Nor can it do so without a function that can construct (or pass on) strict elements, hence the '!' on the result type of the parameter function (so 'mapS (const undefined)' won't typecheck, either). Since there are no ways of producing an arbitrary '!a' out of thin air, polymorphic parameter functions will have type '!a->!a' (if 'a' gets specialised, eg to 'Int', then trivial 'Int->!Int' functions are possible).
Being conjured out of thin air, none of this might not hold up under closer scrutiny, but papers like [1] suggest that it isn't entirely out of reach - further references or counterexamples appreciated!-)
I don't think there's any realistic way to keep his equation from breaking. For instance, you might be able to prevent someone from writing: f :: !a -> !a f _ = undefined However, that still doesn't guarantee that you can't write non-terminating functions, which are semantically bottom: f :: !a -> !a f a = f a Note, that you can even write non-termination for unboxed types: n :: Int# n = n Even though such values may be supposedly unlifted. So, given that second f, clearly length (map f xs) = _|_ when length xs > 1. Total languages go through a great deal of effort to prevent this sort of thing. For instance, many use syntactic checks on the functions your write to ensure that they are structurally recursive. So, perhaps you could add these checks to a Haskell compiler, but you'd also have to ensure that you don't produce total values from non-total values, because doing structural recursion over coinductive values (like infinite lists) introduces bottom. And finally, you'd have to do similar checks on Haskell's data types, because the unrestricted recursive types that Haskell has allow you to introduce bottom without explicit recursion: newtype Wrap a = Roll { unRoll :: Wrap a -> a } -- (\x -> x x) (\x -> x x) omega :: a omega = w (Roll w) where w x = unRoll x x The solution most total languages take is to make sure that all such recursive types are strictly positive (recursive uses of the type may not be to the left of an arrow; Wrap clearly fails this check). Anyhow, it seems to me that to adequately separate all this stuff, and prevent things like 'length xs = length (mapS f xs)' from breaking, you'd end up with an entirely separate total sublanguage that doesn't interact much with the existing part (which kind of ruins the appeal of introducing such annotations in the first place). Perhaps I'm missing something, though. Cheers, Dan