[Haskell-cafe] is 256M RAM insufficient for a 20 millionelementInt/Int map?

[Dan Doel]

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