2017-08-04 16 views
26

私は現在Type-Driven Development with Idrisの本を使っています。はidrisの型を含む型でインデックスされています

第6章では、サンプルデータストアの設計に関する2つの質問があります。データストアは、コマンドラインアプリケーションで、ユーザーはその中に格納されているデータの種類を設定して新しいデータを追加できます。

ここにコードの関連部分を示します(わずかに簡略化)。あなたはGithubの上full codeを見ることができます:

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 

これは理にかなっていて使いやすいですが、一つのことは、デザインについての私を盗聴しました。 DataStoreSchemaが含まれているのはなぜですか?でインデックスされていますか?

DataStoreのでSchemaでインデックス付けされていない、我々は次のように間違ったaddToStore機能を記述することができ:

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

は、私は次のようになり、より安全なタイプのコードを想像するものです。あなたはGithubの上full codeを見ることができます:

  1. なぜ本はDataStoreタイプ(のより多くのタイプセーフなバージョンを使用していませんでした。ここで

    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つはSchemaで索引付けされています)より安全性の低いバージョン(Schemaを含むバージョン)を使用することで得られるものはありますか?

  2. 他のタイプのインデックスが付けられているタイプの理論的な違いは何ですか?この違いは、あなたが取り組んでいる言語に応じて変化しますか?

    例えば、私はIdrisに大きな違いはないと思うが、Haskellには大きな違いがある。 (右...?)

    私はちょうどIdrisで遊んで始めました(そして、私は特にHaskellでシングルトンやGADTの使い方に精通していません)ので、私は周りを頭で囲むのに苦労していますこの。もしこれについて話している論文を私に指摘できれば、私は非常に興味があります。

+1

@ShershとOP:作者は実際に本の後半で実際にこの移行を正確に行いました(10.3.2節参照)。ここに[本のコード]があります(https://github.com/edwinb/TypeDD-Samples/blob/a5c08a13e6a6ec804171526aca10aae946588323/Chapter10/DataStore.idr#L17) –

+0

@AntonTrunovこれは、この変換が優れていることを証明しています。おそらく最初のものが擬似性のために選択されたでしょう。 – Shersh

+0

@Shershうーん、私は主に味の問題だと思う。私は、個人的には、その使用法に関するいくつかの補題を持つより単純なデータ型を好むでしょう。このようにしてコードを記述し、後でそれについてのいくつかのプロパティを証明することができます。リストを使用したり、ML-(またはHaskell-)スタイルを書いたり、後でそれらについて何かを証明したり、ベクトルとしてそのような悪名高いデータ型を使うことができます。私は、異質な平等、別名ジョン・メジャー・イコール)を使用しないことを意味します。例えば、 [この回答](https://stackoverflow.com/a/30159566/2747511)。 –

答えて

0

コメントによると、これはpedantryでした。初期には、従属レコードが使用されるため、型索引を扱う必要はありません。後で、有効な実装を制限する(そして校正検索で見つけやすくする)ために、インデックス付きの型が使用されます。

関連する問題