Индексируется по типу против содержащему тип в idris

Question

В настоящее время я прорабатываю разработку с использованием типов с книгой 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 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:

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. Почему в книге не использовалась более безопасная версия DataStore тип (тот, который индексируется Schema)? Есть ли что-то, что можно получить, используя менее типобезопасную версию (ту, которая просто содержит Schema)?

2. Какова теоретическая разница между типом, индексируемым другим типом, и другим типом? Меняется ли эта разница в зависимости от того, на каком языке вы работаете?

   Например, я думаю, что в Идрисе не может быть большой разницы, но в Хаскеле есть большая разница. (Правильно...?)

   Я только начал играть с Idris (и я не особо разбираюсь в использовании синглетонов или GADT в Haskell), поэтому мне трудно обдумать это. Если бы вы могли указать мне на какие-либо газеты об этом, мне было бы очень интересно.

Answer 1

Согласно комментариям, это была педантичность. Вначале используется зависимая запись, так что работа с индексами типов не требуется. Позже, индексированный тип используется, чтобы ограничить (и сделать его легче найти через пробный поиск) допустимые реализации.