types - img - meta alt tag

indexado por un tipo vs que contiene un tipo en idris

Question

Actualmente estoy revisando el libro Type-Driven Development with Idris .

Tengo dos preguntas relacionadas con el diseño del almacén de datos de ejemplo en el Capítulo 6. El almacén de datos es una aplicación de línea de comandos que permite al usuario establecer qué tipo de datos se almacenan en él y luego agregar datos nuevos.

Aquí están las partes relevantes del código (simplificado ligeramente). Puedes ver el código completo en 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

Esto tiene sentido y es fácil de usar, pero una cosa me molestó en el diseño. ¿Por qué el DataStore contiene un Schema lugar de estar indexado por uno ?

Debido a que el DataStore no está indexado por un Schema , podríamos haber escrito una función de addToStore incorrecta como esta:

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

Esto es lo que me imagino que se vería con más código de código seguro. Puedes ver el código completo en 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

Aquí están mis dos preguntas:

1. ¿Por qué el libro no utilizó la versión más segura para el tipo del tipo DataStore (la indexada por el Schema )? ¿Hay algo que se gana usando la versión menos segura para el tipo (la que solo contiene un Schema )?

2. ¿Cuál es la diferencia teórica de un tipo que está siendo indexado por otro tipo frente a otro tipo? ¿Esta diferencia cambia según el idioma en el que está trabajando?

   Por ejemplo, imagino que podría no haber una gran diferencia en Idris, pero hay una gran diferencia en Haskell. (Derecha...?)

   Simplemente empecé a jugar con Idris (y no estoy particularmente versado en el uso de singletons o GADTs en Haskell), así que me cuesta mucho darme cuenta de esto. Si pudiera señalarme algún documento que hablara de esto, estaría muy interesado.

Answer 1

Por los comentarios, esto fue pedantería. Al principio, se utiliza un registro dependiente para que no sea necesario tratar con índices de tipo. Más tarde, se usa un tipo indexado para restringir (y facilitar la búsqueda mediante pruebas de búsqueda) implementaciones válidas.