按类型索引与包含 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 commandn", dataStore)
Just (SetSchema newSchema) =>
Just ("updated schema and reset datastoren", 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而不是由编制索引？

因为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 commandn", (_ ** MkData size' items'))
Just (SetSchema newSchema) =>
Just ("updated schema and reset datastoren", (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. 一个类型被另一个类型索引与包含另一个类型有什么理论区别？ 这种差异会根据您正在使用的语言而改变吗？

   例如，我想伊德里斯可能没有太大的不同，但哈斯克尔有很大的不同。(对...？

   我刚开始玩伊德里斯(而且我对在哈斯克尔中使用单例或GADT并不是特别精通(，所以我很难理解这一点。 如果你能指出我任何谈论这个问题的论文，我会非常感兴趣。

Answer 1

根据评论，这是迂腐。 早期，使用依赖记录，以便不需要处理类型索引。 稍后，将使用索引类型来限制(并通过校对搜索更容易找到(有效实现。