はidrisの型を含む型でインデックスされています

Question

私は現在Type-Driven Development with Idrisの本を使っています。

第6章では、サンプルデータストアの設計に関する2つの質問があります。データストアは、コマンドラインアプリケーションで、ユーザーはその中に格納されているデータの種類を設定して新しいデータを追加できます。

ここにコードの関連部分を示します（わずかに簡略化）。あなたは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 _ [] 

は、私は次のようになり、より安全なタイプのコードを想像するものです。あなたはGithubの上full codeを見ることができます：

1. なぜ本はDataStoreタイプ（のより多くのタイプセーフなバージョンを使用していませんでした。ここで

   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つはSchemaで索引付けされています）より安全性の低いバージョン（Schemaを含むバージョン）を使用することで得られるものはありますか？

2. 他のタイプのインデックスが付けられているタイプの理論的な違いは何ですか？この違いは、あなたが取り組んでいる言語に応じて変化しますか？

   例えば、私はIdrisに大きな違いはないと思うが、Haskellには大きな違いがある。 （右...？）

   私はちょうどIdrisで遊んで始めました（そして、私は特にHaskellでシングルトンやGADTの使い方に精通していません）ので、私は周りを頭で囲むのに苦労していますこの。もしこれについて話している論文を私に指摘できれば、私は非常に興味があります。

Answer 1

コメントによると、これはpedantryでした。初期には、従属レコードが使用されるため、型索引を扱う必要はありません。後で、有効な実装を制限する（そして校正検索で見つけやすくする）ために、インデックス付きの型が使用されます。