Skype

[Koen Claessen]

[12:01:42 PM CEST] Simon Peyton Jones: hello
[12:01:47 PM CEST] Simon Peyton Jones: no sound
[12:01:56 PM CEST] Simon Peyton Jones: video works
[12:02:17 PM CEST] Koen Claessen: still no sound?
[12:02:20 PM CEST] Simon Peyton Jones: no
[12:02:24 PM CEST] Simon Peyton Jones: plenty of hiss thought
[12:02:25 PM CEST] Koen Claessen: let me restart skype
[12:02:27 PM CEST] Simon Peyton Jones: ok
[12:05:12 PM CEST] Koen Claessen: you, me, dimitrios, nathan, charles-pierre
[12:09:13 PM CEST] Koen Claessen: type classes:
[12:09:27 PM CEST] Koen Claessen: (1) desugared away, so become
higher-order functions
[12:09:36 PM CEST] Koen Claessen: "optmize" using inlining
[12:09:42 PM CEST] Koen Claessen: specializing
[12:09:57 PM CEST] Simon Peyton Jones: f :: Num a => a -> a
[12:10:14 PM CEST] Koen Claessen: forget optimizing
[12:10:23 PM CEST] Koen Claessen: (2) contracts in relationships with
type classes
[12:11:01 PM CEST] Simon Peyton Jones: f :: Num a => a -> [a]
[12:12:06 PM CEST] Simon Peyton Jones: f g x = g x
[12:13:12 PM CEST] Koen Claessen: mapp p f [] = []
[12:13:23 PM CEST] Koen Claessen: mapp p f (x:xs) = f x : mapp p f xs
[12:14:04 PM CEST] Koen Claessen: mappp :: p -> ({ x | p x } -> {y | p
y}) -> { xs | all p xs } -> { ys | all p ys }
[12:15:44 PM CEST] Koen Claessen: objective: take any program
[12:15:55 PM CEST] Koen Claessen: add just enough contract stuff to
show that everything is crash-free
[12:16:31 PM CEST] Simon Peyton Jones: f x = x
[12:16:36 PM CEST] Simon Peyton Jones: f :: CF
[12:16:40 PM CEST] Simon Peyton Jones: f :: CF -> CF
[12:18:07 PM CEST] Koen Claessen: Koen looks this up
[12:18:14 PM CEST] Simon Peyton Jones: "This" = polymorphic CF
[12:18:35 PM CEST] Simon Peyton Jones: (Which is very convenient in
practice, if the ultimate goal is CF-ness.)
[12:18:39 PM CEST] Simon Peyton Jones: eg for type clases
[12:18:48 PM CEST] Koen Claessen: other problem: primitive functions
[12:18:54 PM CEST] Koen Claessen: we need axioms for those
[12:23:53 PM CEST] Simon Peyton Jones: {- CONTRACT foo :: <contract> -}
[12:24:11 PM CEST] Simon Peyton Jones: {- CONTRACT_DEFN foo -}
[12:27:07 PM CEST] Simon Peyton Jones: {- CONTRACR "foo_length" foo ::
<contract> -}
[12:27:28 PM CEST] Koen Claessen: contr_foo_length :: Contract (Int -> Int)
[12:27:47 PM CEST] Simon Peyton Jones: import M( foo, {-# CONTRACT
"foo_length" #-} )
[12:28:22 PM CEST] Simon Peyton Jones: f :: { x | length x > 4 }
[12:28:38 PM CEST] Simon Peyton Jones: f_c1 :: Contract Int
[12:28:48 PM CEST] Koen Claessen: contr_foo_length = Pred (\x -> length x > 4)
[12:31:24 PM CEST] Koen Claessen: (this does not work so well because
the RHS of contracts need to only use constructors)
[12:34:28 PM CEST] Simon Peyton Jones: f (x:y:ys) = e
[12:34:38 PM CEST] Simon Peyton Jones: Into one axiom not two
[12:34:44 PM CEST] Simon Peyton Jones: (one for each pattern match)
[12:37:05 PM CEST] Simon Peyton Jones: Major tasks
1) Implement on real Haskell
[12:37:12 PM CEST] Simon Peyton Jones: 2) Write up what we now know
[12:42:42 PM CEST] Simon Peyton Jones: For (2) one insight is that we
only get "easy quantification"
[12:43:35 PM CEST] Simon Peyton Jones: SMT solvers have built-in theories
[12:43:52 PM CEST] Simon Peyton Jones: SMT solvers only approximate
quantification, whereas FOL deals with quantification comletely
[12:44:19 PM CEST] Simon Peyton Jones: And that allows us to express
Haskell programs in the logic, and hence in our contracts
[12:45:08 PM CEST] Simon Peyton Jones: So SMT solvers are OUT for our
contracts, which include Haskell programs
[12:45:55 PM CEST] Simon Peyton Jones: Also we can inline functions
as-needed, which an SMT solver cannot do
[12:46:51 PM CEST] Simon Peyton Jones: This matters for *recursive*
functions that don't have contrats
[12:48:15 PM CEST] Simon Peyton Jones: Some theories just don't play
nice with full quantification
Eg theory of linear integer arithmetic DOES NOT
theory of lists DOES
[12:48:56 PM CEST] Simon Peyton Jones: So you have to choose: SMT or FOL
[12:57:53 PM CEST] Simon Peyton Jones: Paper idea: translate Haskell +
contracts to FOL, including the min() idea
[12:59:43 PM CEST] Simon Peyton Jones: Translating Haskell to FOL
using min() is already useful
[1:01:15 PM CEST] Simon Peyton Jones: Then add contracts; it's a
beautiful fit. Amazingly the same miin() works