В настоящее время я просматриваю книгу с поддержкой Idris.
У меня есть два вопроса, касающихся дизайна хранилища примеров в главе 6. Хранилище данных - это приложение командной строки, которое позволяет пользователю устанавливать, какие данные хранятся в нем, а затем добавлять новые данные.
Вот соответствующие части кода (упрощенно). Вы можете увидеть полный код в 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 [email protected](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
не индексируется a Schema
, мы могли бы написать неправильную функцию addToStore
, подобную этой:
addToStore
: (dataStore : DataStore) -> SchemaType (schema dataStore) -> DataStore
addToStore _ newitem =
MkData SInt _ []
Вот что я бы предположил, что будет выглядеть более безопасный код типа. Вы можете увидеть полный код на 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
Вот мои два вопроса:
-
Почему книга не использовала более безопасную версию типа
DataStore
(тот, который был проиндексированSchema
)? Есть ли что-то, что получается при использовании менее безопасной версии (той, которая содержит толькоSchema
)? -
Какова теоретическая разница типа, который индексируется другим типом vs, содержащим другой тип? Изменяется ли это различие в зависимости от того, на каком языке вы работаете?
Например, я полагаю, что в Идрисе не может быть большой разницы, но в Haskell есть большая разница. (Правый...?)
Я только начал играть с Идрисом (и я не очень хорошо разбираюсь в использовании синглонов или GADT в Haskell), поэтому мне сложно сплести голову вокруг этого. Если бы вы могли указать мне на любые бумаги, говорящие об этом, мне было бы очень интересно.