FW: Do we really want CF = CF -> CF?

[Simon Peyton-Jones]

-----Original Message-----
From: Nathan Collins [mailto:nathan....@gmail.com]
Sent: 03 November 2011 22:16
To: Dimitrios Vytiniotis; Simon Peyton-Jones; Koen Claessen (ko...@chalmers.se)
Subject: Do we really want CF = CF -> CF?

Do we really want CF = CF -> CF? Maybe there's a way to place the
'min's that makes it fast, but all the versions I've tried slow things
down a lot (see e.g.
https://github.com/cpa/haskellcontracts/commit/b178be9a69b048d2a0e70baabfe58795805cc73a
for a summary of what happened in the no-min case).

The example Simon likes to give here is 'id':

id x = x
id ::: CF

Supposedly we want CF = CF -> CF because we can use 'id' at many
different types. I think what we really want is polymorphic contracts
for polymorphic functions:

id ::: forall c. c -> c

Of course, I don't know how that would work ... so how about some
crazy talk ... maybe something like

forall f c1 c2. (
sat(f,arr(c1,c2)) <-> forall x. sat(x,c1) -> sat(f x,c2 x)) --
contracts can also be functions! Dependency is implicit in
'arr(c1,c2)'.

forall e. sat(e,CF) <-> cf(e)

forall e x p. sat(e,pred(p)) <-> (e /= UNR -> p x = True \/ p x = BAD)

... and it becomes complicated quickly. E.g. consider '($)':

f $ x = f x -- writing '($) = id' would obscure the point here?
-- ??? not sure how to treat 'x' here.
f ::: forall c1,c2[x]. (x:c1 -> c2) -> x:c1 -> c2
-- ??? Maybe as above: in 'c0 -> ... -> cn' have 'ck' a function
'\x0...xk-1.c' ?
f ::: forall c1, c2. (c1 -> c2) -> const c1 -> const c2
-- or
f ::: forall c1, c2. (c1 -> c2) -> const (c1 -> c2)

See https://github.com/cpa/haskellcontracts-examples/blob/master/yes/map.hs
for a really fanciful contract. We'd have to draw the line
somewhere...

Cheers,

-nathan