indeksowana przez typ kontra zawierająca typ w idriscie

Question

W tej chwili przeglądam książkę Type-Driven Development with Idris.

Mam dwa pytania dotyczące projektowania przykładowej składnicy danych w rozdziale 6. Magazyn danych to aplikacja wiersza poleceń, która pozwala użytkownikowi ustawić, jakie dane są w niej przechowywane, a następnie dodać nowe dane.

Oto odpowiednie części kodu (nieco uproszczone). Można zobaczyć full code na 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 

to sens i jest łatwy w obsłudze, ale jedno podsłuch mi o projekcie. Dlaczego DataStore zawiera Schema zamiast być indeksowane przez jeden?

Ponieważ DataStore nie jest indeksowana przez Schema, moglibyśmy napisany nieprawidłową addToStore funkcję tak:

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

Oto co bym sobie wyobrazić bardziej bezpieczne typu kod będzie wyglądać. Można zobaczyć full code na 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 

---

Oto moje dwa pytania:

1. Dlaczego nie książka używać bardziej type-safe wersję typu DataStore (The jeden indeksowany przez Schema)? Czy jest coś, co zyskuje się, używając mniej bezpiecznej wersji (tej, która zawiera tylko Schema)?

2. Jaka jest teoretyczna różnica typu indeksowanego przez inny typ kontra zawierającego inny typ? Czy ta różnica zmienia się w zależności od języka, nad którym pracujesz?

   Na przykład, wyobrażam sobie, że może nie być dużej różnicy w Idrisie, ale Haskell ma dużą różnicę. (Dobrze ...?)

   Właśnie zacząłem bawić się z Idrisem (i nie jestem szczególnie dobrze zorientowany w użyciu singletonów lub GADTów w Haskell), więc trudno mi zawijać głowę to. Gdybyś mógł wskazać mi jakieś referaty na ten temat, byłbym bardzo zainteresowany.

Answer 1

Za komentarze, to była pedanteria. Na początku wykorzystywany jest rekord zależny, aby nie trzeba było zajmować się indeksami typu. Później, indeksowany typ jest używany w celu ograniczenia (i ułatwienia wyszukiwania za pomocą wyszukiwania) ważnych implementacji.