编译器能否在 Idris 中隐式找到证明？

Question

我正在尝试学习 Idris 和一般的依赖类型编程。

我正在纠结的是以下想法。假设我创建了这个类型：

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)

这是一种字典，其字段由类型为 String 的键标识，我将与给定键关联的字段类型存储在此 [(String, Type)] 列表中。

我想编写一个函数，给定一个 key: String 我可以以某种方式证明它在列表中，我可以检索存储在该键下的值。

我的尝试是这样的：

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

现在，回答我的问题。

我可以很容易地使用这个函数 get 通过提供足够的类型证据 Contains f a fs:

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


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

但看起来可以自动找到该证据。可以自动化吗？因为使用哪些证据对程序员来说是如此明显，以至于编译器看起来肯定足够聪明，可以找到它。这可能吗？

编辑：

我开始意识到，也许如果记录有两个同名的字段，这将在我面前爆炸...也许 [(String, Type)] 列表不是最好的抽象使用.

Answer 1

Idris 可以用 auto 搜索证明，参见 the docs。在你的情况下，你只需要将 get 的类型更改为

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

然后 Idris 会在调用 get 时尝试在 compile-time 构造一个证明，但如果需要，您仍然可以使用 get {p=T H} 来明确。

另外请注意，如果您定义 Nil 和 (::)（而不是 Cons），Idris 支持列表的语法糖。所以你可以美化一些东西，比如：

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]

您还可以根据您的 use-case，将 Contains s a fs 简化为 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.

如果你想保证你的 Rec 中只有一个键，你可以使用类似的东西：

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)

但是你可能需要一个单独的构造函数，因为 Idris 不是很擅长证明 Not t。 :-)

如果你想要练习，你可以尝试实现一个类似的工作 Rec 作为：

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)

编译器能否在 Idris 中隐式找到证明？

Can the compiler find proofs implicitly in Idris?

dependent-type

idris