được lập chỉ mục theo loại so với chứa loại trong idris

Question

Tôi hiện đang trải qua cuốn sách Type-Driven Development with Idris.

Tôi có hai câu hỏi liên quan đến thiết kế kho dữ liệu ví dụ trong Chương 6. Kho dữ liệu là một ứng dụng dòng lệnh cho phép người dùng đặt loại dữ liệu nào được lưu trữ trong đó, sau đó thêm dữ liệu mới.

Dưới đây là các phần có liên quan của mã (được đơn giản hóa một chút). Bạn có thể xem full code trên 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 

này có ý nghĩa và rất dễ dàng để sử dụng, nhưng có một điều nghe trộm tôi về thiết kế. Tại sao DataStore chứa Schema thay vì được lập chỉ mục bởi một?

Vì DataStore không được lập chỉ mục bởi một Schema, chúng ta có thể viết một addToStore chức năng không chính xác như thế này:

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

Dưới đây là những gì tôi tưởng tượng nhiều loại mã an toàn sẽ trông như thế nào. Bạn có thể xem full code trên 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 

---

Dưới đây là hai câu hỏi của tôi:

1. Tại sao không phải là cuốn sách sử dụng các loại an toàn phiên bản nhiều loại DataStore (các được lập chỉ mục bởi Schema)? Có điều gì đó đạt được bằng cách sử dụng phiên bản ít an toàn hơn (phiên bản chỉ chứa Schema) không?

2. Sự khác biệt về mặt lý thuyết của loại được lập chỉ mục bởi loại khác so với loại khác? Sự khác biệt này có thay đổi tùy thuộc vào ngôn ngữ bạn đang làm việc không?

   Ví dụ, tôi tưởng tượng có thể không có sự khác biệt lớn trong Idris, nhưng có một sự khác biệt lớn trong Haskell. (Phải ...?)

   Tôi vừa mới bắt đầu chơi với Idris (và tôi không đặc biệt thành thạo với việc sử dụng các single hoặc GADT trong Haskell), vì vậy tôi đang gặp khó khăn trong đầu điều này. Nếu bạn có thể chỉ cho tôi bất kỳ giấy tờ nói về điều này, tôi sẽ rất quan tâm.

Answer 1

Mỗi nhận xét, đây là bộ hành. Sớm, một hồ sơ phụ thuộc được sử dụng để đối phó với các chỉ số loại là không cần thiết. Sau đó, một loại được lập chỉ mục được sử dụng để hạn chế (và thực hiện dễ dàng hơn thông qua việc thực hiện tìm kiếm bằng chứng) hợp lệ.