idris - 编译器能否在 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)] list 并不是最好的抽象。

Answer 1

Idris 可以使用 auto 搜索证明，见 the docs .在您的情况下，您只需要更改 get 的类型到

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

然后，Idris 在调用 get 时尝试在编译时构建证明。 ，但你仍然可以明确地使用 get {p=T H}如果你需要。

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

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]

您还可以根据您的用例简化 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里只有一把 key ，你可以使用类似的东西:

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)