Can the compiler find proofs implicitly in Idris?

Question

I'm trying to learn Idris and dependently typed programming in general.

What I'm struggling with is the following idea. Suppose I create this types:

data Entry: String -> a -> Type where
  E: (name: String) -> (value: a) -> Entry name a

data Rec: List (String, Type) -> Type where
  Nil: Rec []
  Cons: Entry s a -> Rec ts -> Rec ((s, a) :: ts)

myRec: Rec [("name", String), ("age", Integer)]
myRec = Cons (E "name" "Rafael") (Cons (E "age" 35) Nil)

This is kind of a dictionary, whose fields are identified by a key of type String and I store the type of the field associated with a given key in this [(String, Type)] list.

I wanted to write a function that, given a key: String that I can somehow prove that are in the list, I can retrieve the value stored under that key.

My attempt is this:

data Contains : String -> Type -> List (String, Type) -> Type where
  H : Contains s a ((s, a) :: ts)
  T : Contains s a xs -> Contains s a (x :: xs)

getFieldType : {a: Type}
            -> (f: String)
            -> (fs: List (String, Type))
            -> (Contains f a fs)
            -> Type
getFieldType f ((f, a) :: xs) H = a
getFieldType f (_ :: xs) (T y) = getFieldType f xs y

get : (f: String) -> Rec fs -> getFieldType f fs p
get {p = H} f (Cons (E f value) y) = value
get {p = (T z)} f (Cons _ y) = get {p=z} f y

Now, to my question.

I can easily use this function get by providing an adequate evidence of type Contains f a fs:

*src/test> get {p=H} "name" myRec
"Rafael" : String


*src/test> get {p=T H} "age" myRec
35 : Integer

But it looks like that finding this evidence could be automated. Can it be automated? Because which evidence to use is so obvious for the programmer that it surely looks like the compiler is smart enough to find it. Is that possible?

EDIT:

I'm starting to realize that maybe if the record has two fields with the same name this is going to explode in my face... Maybe the [(String, Type)] list wasn't the best abstraction to use.

xash xash · Accepted Answer · 2018-02-20T00:36:17

Idris can search for proofs with auto, see the docs. In your case, you only need to change the type of get to

get : (f : String) -> Rec fs -> {auto p : Contains f a fs} -> getFieldType f fs p

Then Idris tries to construct a proof at compile-time when calling get, but you can still be explicit with get {p=T H} if you need to.

Another note, Idris supports syntactic sugar for lists if you define Nil and (::) (instead of Cons). So you can prettify some things like:

data Rec: List (String, Type) -> Type where
  Nil : Rec []
  (::) : Entry s a -> Rec ts -> Rec ((s, a) :: ts)

data Contains : String -> Type -> List (String, Type) -> Type where
  H : Contains s a ((s, a) :: ts)
  T : Contains s a xs -> Contains s a (x :: xs)

myRec: Rec [("name", String), ("age", Integer)] 
myRec = [E "name" "Rafael", E "age" 35]

You can also, depending on your use-case, simplify Contains s a fs to Contains s fs.

I'm starting to realize that maybe if the record has two fields with the same name this is going to explode in my face... Maybe the [(String, Type)] list wasn't the best abstraction to use.

If you want to guarantee that there is only one key in your Rec, you could use something like:

data Contains : String -> Type -> List (String, Type) -> Type where
  H : Contains s a ((s, a) :: ts)
  T : Contains s a xs -> Contains s a (x :: xs)

data Rec: List (String, Type) -> Type where
  Nil : Rec []
  (::) : Entry s a -> Rec ts -> {p : Not (Contains s a ts)} -> Rec ((s, a) :: ts)

But than you'd probably need a seperate constructor function, because Idris isn't very good at proving Not t. :-)

If you want an exercise, you could try to implement a similar working Rec as:

data Rec : Vect k String -> Vect k Type -> Type where
  Empty : Rec [] []
  Add : {ty : Type} -> (k : String) -> (v : ty) -> Rec ks tys -> Rec (k :: ks) (ty :: tys)

Can the compiler find proofs implicitly in Idris?

1 Answers