indexé par un type vs contenant un type dans idris

Question

Je suis en train de parcourir le livre Type-Driven Development with Idris. J'ai deux questions relatives à la conception de l'exemple de magasin de données au chapitre 6. Le magasin de données est une application en ligne de commande qui permet à l'utilisateur de définir le type de données stockées, puis d'ajouter de nouvelles données.

Voici les parties pertinentes du code (légèrement simplifié). Vous pouvez voir le full code sur 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 

Cela est logique et est facile à utiliser, mais une chose me buggé au sujet de la conception. Pourquoi le DataStore contient-il un Schema au lieu d'être indexé par un?

Parce que le DataStore n'est pas indexé par un Schema, on aurait pu écrire une fonction addToStore incorrecte comme ceci:

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

Voici ce que j'imagine plus un code de type sécurité ressemblerait. Vous pouvez voir la full code sur 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 

---

Voici mes deux questions:

1. Pourquoi ne pas le livre utiliser la version plus de type sécurisé du type DataStore (la un indexé par le Schema)? Y at-il quelque chose qui est gagné en utilisant la version moins sécurisée (celle qui contient juste un Schema)?

2. Quelle est la différence théorique entre un type indexé par un autre type et un autre type? Est-ce que cette différence change en fonction de la langue sur laquelle vous travaillez? Par exemple, j'imagine qu'il n'y a peut-être pas de grande différence dans Idris, mais il y a une grosse différence dans Haskell. (Juste ...?)

   Je viens de commencer à jouer avec Idris (et je ne suis pas particulièrement familier avec l'utilisation de singletons ou de GADTs dans Haskell), donc j'ai du mal à faire le tour ce. Si vous pouviez me montrer des articles sur ce sujet, je serais très intéressé.

Answer 1

Par les commentaires, c'était pedantry. Très tôt, un enregistrement dépendant est utilisé de sorte qu'il n'est pas nécessaire de traiter les index de type. Plus tard, un type indexé est utilisé afin de restreindre (et de faciliter la recherche via proof-search) les implémentations valides.