按类型索引与在 Idris 中包含类型的区别

Question

我是一名有用的助手，可以为您翻译文本。

我目前正在学习使用Idris进行类型驱动开发这本书。

我有两个问题与第6章中示例数据存储的设计有关。该数据存储是一个命令行应用程序，允许用户设置存储在其中的数据类型，然后添加新数据。

以下是相关代码的部分内容（稍作简化）。 您可以在Github上查看完整代码：

module Main

import Data.Vect

infixr 4 .+.

-- This datatype is to define what sorts of data can be contained in the data store.
data Schema
  = SString
  | SInt
  | (.+.) Schema Schema

-- This is a type-level function that translates a Schema to an actual type.
SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

-- This is the data store.  It can potentially be storing any sort of schema.
record DataStore where
       constructor MkData
       schema : Schema
       size : Nat
       items : Vect size (SchemaType schema)

-- This adds new data to the datastore, making sure that the new data is
-- the same type that the DataStore holds.
addToStore
  : (dataStore : DataStore) -> SchemaType (schema dataStore) -> DataStore
addToStore (MkData schema' size' store') newitem =
  MkData schema' _ (addToData store')
  where
    addToData
      : Vect size' (SchemaType schema') -> Vect (size' + 1) (SchemaType schema')
    addToData xs = xs ++ [newitem]

-- These are commands the user can use on the command line.  They are able
-- to change the schema, and add new data.
data Command : Schema -> Type where
  SetSchema : (newSchema : Schema) -> Command schema
  Add : SchemaType schema -> Command schema

-- Given a Schema, this parses input from the user into a Command.
parse : (schema : Schema) -> String -> Maybe (Command schema)

-- This is the main workhorse of the application.  It parses user
-- input, turns it into a command, then evaluates the command and 
-- returns an updated DataStore.
processInput
  : (dataStore : DataStore) -> String -> Maybe (String, DataStore)
processInput dataStore@(MkData schema' size' items') input =
  case parse schema' input of
    Nothing => Just ("Invalid command\n", dataStore)
    Just (SetSchema newSchema) =>
      Just ("updated schema and reset datastore\n", MkData newSchema _ [])
    Just (Add item) =>
      let newStore = addToStore (MkData schema' size' items') item
      in Just ("ID " ++ show (size dataStore) ++ "\n", newStore)

-- This kicks off processInput with an empty datastore and a simple Schema
-- of SString.
main : IO ()
main = replWith (MkData SString _ []) "Command: " processInput

这很合理且易于使用，但是设计中有一件事情让我感到困扰。为什么DataStore包含一个Schema而不是由一个Schema进行索引？

因为DataStore没有被Schema索引，所以我们可能会编写一个不正确的addToStore函数，例如：

addToStore
  : (dataStore : DataStore) -> SchemaType (schema dataStore) -> DataStore
addToStore _ newitem =
  MkData SInt _ []

这是我想象中更加类型安全的代码。你可以在Github上看到完整代码：

module Main

import Data.Vect

infixr 4 .+.

data Schema
  = SString
 | SInt
 | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

record DataStore (schema : Schema) where
       constructor MkData
       size : Nat
       items : Vect size (SchemaType schema)

addToStore
  : (dataStore : DataStore schema) ->
    SchemaType schema ->
    DataStore schema
addToStore {schema} (MkData size' store') newitem =
  MkData _ (addToData store')
  where
    addToData
      : Vect size' (SchemaType schema) -> Vect (size' + 1) (SchemaType schema)
    addToData xs = xs ++ [newitem]

data Command : Schema -> Type where
  SetSchema : (newSchema : Schema) -> Command schema
  Add : SchemaType schema -> Command schema

parse : (schema : Schema) -> String -> Maybe (Command schema)

processInput
  : (schema : Schema ** DataStore schema) ->
    String ->
    Maybe (String, (newschema ** DataStore newschema))
processInput (schema ** (MkData size' items')) input =
  case parse schema input of
    Nothing => Just ("Invalid command\n", (_ ** MkData size' items'))
    Just (SetSchema newSchema) =>
      Just ("updated schema and reset datastore\n", (newSchema ** MkData _ []))
    Just (Add item) =>
      let newStore = addToStore (MkData size' items') item
          msg = "ID " ++ show (size newStore) ++ "\n"
      in Just (msg, (schema ** newStore))

main : IO ()
main = replWith (SString ** MkData _ []) "Command: " processInput

---

这里有两个问题：

1. 为什么这本书没有使用更安全的 DataStore 类型（由 Schema 索引）？使用不太安全的版本（只包含一个 Schema）是否会有所收获？

2. 一个类型被另一个类型索引与包含有何理论区别？这种区别是否取决于您正在使用的编程语言？

   例如，我想在 Idris 中可能没有太大的区别，但在 Haskell 中可能有很大的区别。（是吗...？）

   我刚开始尝试 Idris（并不是特别熟悉 Haskell 中单例或 GADTs 的用法），所以我很难理解这个问题。如果您可以指向任何论文来讨论这个问题，我会非常感兴趣。

- illabout

---

@Shersh 和 OP：作者实际上在书的后面（见第10.3.2节）做了这个转换。这是书中的代码。 - Anton Trunov

@AntonTrunov 这证明了这种转换更好。也许第一个是因为简单而被选择的。 - Shersh

@Shersh 嗯，我认为这主要是品味问题。就我个人而言，我更喜欢一个简单的数据类型，并有关于其使用的几个引理。这样，您可以编写代码，然后稍后证明一些关于它的属性。例如，您可以使用列表，编写ML（或Haskell）风格的程序，然后稍后证明其中的某些内容，或者您可以使用诸如向量之类的臭名昭著的数据类型，在这种情况下，有时甚至无法声明有关其值的属性（我的意思不是使用异构相等性，也就是约翰·梅杰相等性）。请参见，例如此答案。 - Anton Trunov

@AntonTrunov 这本书后面确实使用了转换，但它指出：“与其将模式存储为记录中的字段，这里你通过数据的模式对记录进行参数化，因为你不打算允许更新模式。”（第10.3.2节）我不理解这个评论。在我上面发布的代码中，存储正在通过模式进行参数化，但仍然可以使用相关对来更改。 - illabout

我仍然对数据构造函数“包含”值与数据类型由值（类型？）参数化之间的理论关系感兴趣。此外，它在依赖类型语言（Idris）和非依赖类型语言（Haskell）中的区别如何。 - illabout

@illabout 这个注释的意思是，例如addToStore不能更改输出数据存储的模式。要更改模式，您需要使用一些外部机制，例如依赖对，这样可以明确您更改模式的意图，而在代码的先前版本中并非如此。 - Anton Trunov

Answer 1

根据评论，这是一种迂腐的行为。早期使用依赖记录以避免处理类型索引。后来使用了索引类型，以限制（并更容易通过证明搜索找到）有效的实现。

- Boyd Stephen Smith Jr.