Type-directed search with dependent types
Ben Sherman
August 12, 2014
Types have the potential to be, all at once, specifications, documentation, and proofs of correctness. Because Haskell's got a powerful type system, Hoogle, a tool for finding terms by approximate type signature, proves rather valuable. But in a dependently typed language, types reach their pinnacle. The combined variety and precision of types in such languages means that type-directed search is a really enticing proposition.
So I decided to create such a type-directed search! I wrote the :search function for Idris, a dependently typed programming language inspired by Haskell. I took an approach guided by type isomorphism (which is somewhat different from Hoogle): when :search matches two types, one can be constructed from the other.
This is a talk which I gave at the Haskell DC meetup in Washington, D.C on August 12, 2014.
In the first part of the talk, I discuss how programming languages vary in terms of what can be ascertained statically about their programs, particularly in regards to type systems. When type systems are powerful, as they are in Idris, I prefer type-driven development to test-driven development. I demonstrate that the property map f . map g = map (f . g) is false for ML but prove its veracity for Haskell by hand.
1 import Control.Monad ((<=<))
2 import System.IO (withFile, IOMode (ReadMode), hGetChar, Handle)
3
4
5
6
7 main :: IO ()
8 main = do
9 putStrLn "read1:"
10 f read1
11 putStrLn "read2:"
12 f read2
13 where
14 f reader = withFile "haskell.txt" ReadMode $ \h -> do
15 xs <- reader h [1..30]
16 putStrLn xs
17
18
19
20 read1 :: Handle -> [a] -> IO String
21 read1 h = mapM (get <=< get) where
22 get = const (hGetChar h)
23
24
25 read2 :: Handle -> [a] -> IO String
26 read2 h = mapM get <=< mapM get
27 where get = const (hGetChar h)
1 map :: (a -> b) -> [a] -> [b]
2 map f [] = []
3 map f (x : xs) = f x : map f xs
4
5 (.) :: (b -> c) -> (a -> b) -> (a -> c)
6 (.) f g x = f (g x)
7
8
9 ===============================
10
11 (map f . map g) []
12 (.) (map f) (map g) []
13 (map f) (map g [])
14 map f []
15 []
16
17 map (f . g) []
18 []
19
20 ===============================
21
22 (map f . map g) (x : xs)
23 (.) (map f) (map g) (x : xs)
24 (map f) (map g (x : xs))
25 map f (g x : map g xs)
26 f (g x) : map f (map g xs)
27
28
29 map (f . g) (x : xs)
30 (f . g) x : map (f . g) xs
31 f (g x) : map (f . g) xs
32
In the second part of the talk, I construct a term in Idris which bears witness to the fact that map f . map g = map (f . g) is true in Idris. I demonstrate the :search feature in Idris and explain how it works. I also discuss some strategies I employed and issues I faced when developing :search, and ways in which :search can be improved in the future.
1 eqList : {a : Type} -> {x, y : a} -> {xs, ys : List a}
2 -> x = y -> xs = ys -> x :: xs = y :: ys
3 eqList {x} {y} {xs} {ys} p q = replace {P=\ts => x :: xs = y :: ts} q
4 (replace {P=\t => x :: xs = t :: xs} p (refl {x :: xs}))
5
6
7
8
9 mapFusion : {a, b, c : Type}
10 -> (f : a -> b) -> (g : b -> c) -> (xs : List a)
11 -> map (g . f) xs = map g (map f xs)
12 mapFusion f g [] = refl
13 mapFusion f g (x :: xs) = eqList refl (mapFusion f g xs)
14
Idris> :s Type -> Type
= Prelude.Algebra.AbelianGroup : Type -> Type
Sets equipped with a single binary operation that is associative
and commutative, along with a neutral element for that binary
operation and inverses for all elements. Must satisfy the
following laws:
= Prelude.Algebra.BoundedJoinSemilattice : Type -> Type
Sets equipped with a binary operation that is commutative,
associative and idempotent and supplied with a neutral element.
Must satisfy the following laws:
= Prelude.Algebra.BoundedLattice : Type -> Type
Sets equipped with two binary operations that are both
commutative, associative and idempotent and supplied with
neutral elements, along with absorbtion laws for relating the
two binary operations. Must satisfy the following:
= Prelude.Algebra.BoundedMeetSemilattice : Type -> Type
Sets equipped with a binary operation that is commutative,
associative and idempotent and supplied with a neutral element.
Must satisfy the following laws:
= Prelude.Basics.Dec : Type -> Type
Decidability. A decidable property either holds or is a
contradiction.
= Decidable.Equality.DecEq : Type -> Type
Decision procedures for propositional equality
= Prelude.Enum : Type -> Type
= Prelude.Classes.Eq : Type -> Type
The Eq class defines inequality and equality.
= Foreign : Type -> Type
= Prelude.Algebra.Group : Type -> Type
Sets equipped with a single binary operation that is
associative, along with a neutral element for that binary
operation and inverses for all elements. Must satisfy the
following laws:
= IO : Type -> Type
= Inf : Type -> Type
Recursive parameters to codata. Inserted automatically by the
elaborator on a "codata" definition but is necessary by hand if
mixing inductive and coinductive parameters.
= Prelude.Classes.Integral : Type -> Type
= Prelude.Algebra.JoinSemilattice : Type -> Type
Sets equipped with a binary operation that is commutative,
associative and idempotent. Must satisfy the following laws:
= Prelude.Algebra.Lattice : Type -> Type
Sets equipped with two binary operations that are both
commutative, associative and idempotent, along with absorbtion
laws for relating the two binary operations. Must satisfy the
following:
= Lazy : Type -> Type
Lazily evaluated values. This has special evaluation semantics.
= Prelude.List.List : Type -> Type
Linked lists
= Prelude.Classes.MaxBound : Type -> Type
= Prelude.Maybe.Maybe : Type -> Type
= Prelude.Algebra.MeetSemilattice : Type -> Type
Sets equipped with a binary operation that is commutative,
associative and idempotent. Must satisfy the following laws:
= Prelude.Classes.MinBound : Type -> Type
= Prelude.Algebra.Monoid : Type -> Type
Sets equipped with a single binary operation that is
associative, along with a neutral element for that binary
operation. Must satisfy the following laws:
= Prelude.Basics.Not : Type -> Type
= Prelude.Classes.Num : Type -> Type
The Num class defines basic numerical arithmetic.
= Prelude.Classes.Ord : Type -> Type
The Ord class defines comparison operations on ordered data
types.
= PrimIO : Type -> Type
Idris's primitive IO, for building abstractions on top of
= Prelude.Algebra.Ring : Type -> Type
Sets equipped with two binary operations, one associative and
commutative supplied with a neutral element, and the other
associative, with distributivity laws relating the two
operations. Must satisfy the following laws:
= Prelude.Algebra.RingWithUnity : Type -> Type
Sets equipped with two binary operations, one associative and
commutative supplied with a neutral element, and the other
associative supplied with a neutral element, with distributivity
laws relating the two operations. Must satisfy the following
laws:
= Prelude.Algebra.Semigroup : Type -> Type
Sets equipped with a single binary operation that is
associative. Must satisfy the following laws:
= Prelude.Show : Type -> Type
= Prelude.Stream.Stream : Type -> Type
An infinite stream
= Prelude.Uninhabited.Uninhabited : Type -> Type
A canonical proof that some type is empty
= Prelude.Algebra.VerifiedAbelianGroup : Type -> Type
= Prelude.Algebra.VerifiedBoundedJoinSemilattice : Type -> Type
= Prelude.Algebra.VerifiedBoundedLattice : Type -> Type
= Prelude.Algebra.VerifiedBoundedMeetSemilattice : Type -> Type
= Prelude.Algebra.VerifiedGroup : Type -> Type
= Prelude.Algebra.VerifiedJoinSemilattice : Type -> Type
= Prelude.Algebra.VerifiedLattice : Type -> Type
= Prelude.Algebra.VerifiedMeetSemilattice : Type -> Type
= Prelude.Algebra.VerifiedMonoid : Type -> Type
= Prelude.Algebra.VerifiedRing : Type -> Type
= Prelude.Algebra.VerifiedRingWithUnity : Type -> Type
= Prelude.Algebra.VerifiedSemigroup : Type -> Type
= WorldRes : Type -> Type
= (__Elim) : Type -> Type
Type class for eliminators
< assert_total : a -> a
Assert to the totality checker than the given expression will
always terminate.
< Prelude.Basics.id : a -> a
Identity function.
< Prelude.Basics.the : (a : Type) -> a -> a
Manually assign a type to an expression.
< trace_malloc : a -> a
Idris> :s Ord a => List a -> List a
= Prelude.List.sort : Ord a => List a -> List a
< Prelude.List.reverse : List a -> List a
Return the elements of a list in reverse order.
< Prelude.List.nub : Eq a => List a -> List a
< assert_total : a -> a
Assert to the totality checker than the given expression will
always terminate.
< Prelude.Basics.id : a -> a
Identity function.
< Prelude.Basics.the : (a : Type) -> a -> a
Manually assign a type to an expression.
< trace_malloc : a -> a
< Prelude.List.toList : Foldable t => t a -> List a
Convert any Foldable structure to a list.
Idris> :s plus x y = plus y x
= Prelude.Nat.plusCommutative : (left : Nat) ->
(right : Nat) -> left + right = right + left
> Prelude.Nat.multOneLeftNeutral : (right : Nat) ->
fromInteger 1 * right = right
> Prelude.Nat.plusZeroRightNeutral : (left : Nat) ->
left + fromInteger 0 = left
Idris> :t plus
Prelude.Nat.plus : Nat -> Nat -> Nat
Idris> :t the Nat 3
the Nat (fromInteger 3) : Nat
Idris> the Nat 3 + 5
8 : Nat
Idris> :t Vect
Prelude.Vect.Vect : Nat -> Type -> Type
Idris> :t (++)
Prelude.List.(++) : List a -> List a -> List a
Prelude.Strings.(++) : String -> String -> String
Prelude.Vect.(++) : Vect m a -> Vect n a -> Vect (m + n) a
Idris> :t Either
Prelude.Either.Either : Type -> Type -> Type
Idris> :t head
Prelude.List.head : (l : List a) -> (isCons l = True) -> a
Prelude.Stream.head : Stream a -> a
Prelude.Vect.head : Vect (S n) a -> a
Idris> :s Vect (S n) a -> a
= Prelude.Vect.head : Vect (S n) a -> a
Only the first element of the vector
= Prelude.Vect.last : Vect (S n) a -> a
The last element of the vector
Idris> :s Functor f => f a -> f b -> f (a, b)
> Prelude.Vect.zip : Vect n a -> Vect n b -> Vect n (a, b)
Combine two equal-length vectors pairwise
> Prelude.Stream.zip : Stream a -> Stream b -> Stream (a, b)
Create a stream of pairs from two streams
Idris> :s (m, n : Nat) -> m + n = n + m
= Prelude.Nat.plusCommutative : (left : Nat) ->
(right : Nat) -> left + right = right + left
> Prelude.Nat.multOneLeftNeutral : (right : Nat) ->
fromInteger 1 * right = right
> Prelude.Nat.plusZeroRightNeutral : (left : Nat) ->
left + fromInteger 0 = left
Idris> :s Ord a => a -> a -> Bool
= Prelude.Classes.(<) : Ord a => a -> a -> Bool
= Prelude.Classes.(<=) : Ord a => a -> a -> Bool
= Prelude.Classes.(>) : Ord a => a -> a -> Bool
= Prelude.Classes.(>=) : Ord a => a -> a -> Bool
< Prelude.Classes.(/=) : Eq a => a -> a -> Bool
< Prelude.Classes.(==) : Eq a => a -> a -> Bool
> Prelude.Nat.gt : Nat -> Nat -> Bool
Boolean test than one Nat is strictly greater than another
> Prelude.Nat.gte : Nat -> Nat -> Bool
Boolean test than one Nat is greater than or equal to another
> Prelude.Strings.isInfixOf : String -> String -> Bool
> Prelude.Strings.isPrefixOf : String -> String -> Bool
> Prelude.Strings.isSuffixOf : String -> String -> Bool
> Prelude.Nat.lt : Nat -> Nat -> Bool
Boolean test than one Nat is strictly less than another
> Prelude.Nat.lte : Nat -> Nat -> Bool
Boolean test than one Nat is less than or equal to another
Idris> :s fact 5 = the Nat 100
Idris> :s fact 5 = the Nat 120
< Prelude.Nat.maximumZeroNRight : (right : Nat) ->
maximum 0 right = right
< Prelude.Nat.plusOneSucc : (right : Nat) ->
fromInteger 1 + right = S right
< Prelude.Nat.plusZeroLeftNeutral : (right : Nat) ->
fromInteger 0 + right = right
< Prelude.Nat.predSucc : (n : Nat) -> pred (S n) = n
< refl : x = x
A proof that x in fact equals x. To construct this, you must
have already shown that both sides are in fact equal.
Idris> :s (Ord a, Ord b) => (a, b) -> (a, b) -> Bool
< Prelude.Classes.(<) : Ord a => a -> a -> Bool
< Prelude.Classes.(<=) : Ord a => a -> a -> Bool
< Prelude.Classes.(>) : Ord a => a -> a -> Bool
< Prelude.Classes.(>=) : Ord a => a -> a -> Bool
< Prelude.Classes.(/=) : Eq a => a -> a -> Bool
< Prelude.Classes.(==) : Eq a => a -> a -> Bool
View slides in full (PDF).