0
size
returns positive valuesavg
head
and tail
are Safefoldr1
average
map
init
init'
insert
List
s ElementsList
max
type (I)max
type (II)max
type (III)max
typekeys
Map
eval
create
unsafeTake
unpack
chop
Refinement Types for Haskell
With: R. Jhala, E. Seidel, P. Rondon, D. Vytiniotis, S. P. Jones, ...
λ> let average xs = sum xs `div` length xs
λ> average [100, 202, 300]
2
λ> average []
*** Exception: divide by zero
λ> :m +Data.Map
λ> let m = fromList [ ("haskell" , "lazy")
, ("javascript" , "eager")]
λ> m ! "haskell"
"lazy"
λ> m ! "racket"
*** Exception: key is not in the map
λ> sort [1, 2, 3]
[1, 2, 3]
λ> sort [42, 1, 2, 3]
[42]
λ> let fact n = n * fact (n-1)
λ> fact 42
λ> :m + Data.Text Data.Text.Unsafe
λ> let t = pack "CUFP2015"
λ> takeWord16 4 t
"CUFP"
Memory overflows leaking secrets...
λ> takeWord16 20 t
"CUFP2015\2043\9834\1912\3148\NUL\15928\2486\SOH\NUL"
To prevent wider class of errors
To enforce program specific properties
Reason about semantics (apart from structural) properties
Part I: Features
Part II: Case Studies
Refinement Types: Automated Dependent Typing via SMT
Properties: | Predicates + Types |
Proofs: | SMT Solvers + Subtyping |
Inference: | Abstract Interpretation + Hindley-Milner |
Expressiveness
How expressive is decidable logic?
Technology
Applications
http://www.refinement-types.org