索引的類型與包含idris類型

Question

我目前正在通過Type-Driven Development with Idris書。

我在第6章中有兩個與示例數據存儲設計有關的問題。數據存儲是一個命令行應用程序，允許用戶設置存儲哪種數據，然後添加新數據。

以下是代碼的相關部分（稍加簡化）。你可以看到在Github上full code：

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而不是被一個索引？

因爲DataStore不是由Schema索引，我們可以寫一個不正確的addToStore功能是這樣的：

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

這裏是我的想象更安全的代碼會是什麼樣子。你可以看到full code在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有很大的不同。 （Right ...？）

   我剛剛開始與Idris玩耍（我對Haskell中單身人士或GADT的使用並不十分熟悉），所以我很難把頭繞在身邊這個。如果你能指點我的任何文件談論這個，我會非常感興趣。

Answer 1

根據評論，這是pedantry。早期，使用了一個依賴記錄，因此不需要處理類型索引。之後，使用索引類型來限制（並通過證明搜索更容易查找）有效的實現。