The book's Chapter6's datastore:
module Main
import Data.Vect
infixr 5 .+.
data Schema = SString | SInt | (.+.) Schema Schema
SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)
record DataStore where
constructor MkData
schema : Schema
size : Nat
items : Vect size (SchemaType schema)
addToStore : (store : DataStore) -> SchemaType (schema store) -> DataStore
addToStore (MkData schema size store) newitem = MkData schema _ (addToData store)
where
addToData : Vect oldsize (SchemaType schema) -> Vect (S oldsize) (SchemaType schema)
addToData [] = [newitem]
addToData (x :: xs) = x :: addToData xs
setSchema : (store : DataStore) -> Schema -> Maybe DataStore
setSchema store schema = case size store of
Z => Just (MkData schema _ [])
S k => Nothing
data Command : Schema -> Type where
SetSchema : Schema -> Command schema
Add : SchemaType schema -> Command schema
Get : Integer -> Command schema
Quit : Command schema
parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SString input = getQuoted (unpack input)
where
getQuoted : List Char -> Maybe (String, String)
getQuoted ('"' :: xs)
= case span (/= '"') xs of
(quoted, '"' :: rest) => Just (pack quoted, ltrim (pack rest))
_ => Nothing
getQuoted _ = Nothing
parsePrefix SInt input = case span isDigit input of
("", rest) => Nothing
(num, rest) => Just (cast num, ltrim rest)
parsePrefix (schemal .+. schemar) input
= case parsePrefix schemal input of
Nothing => Nothing
Just (l_val, input') =>
case parsePrefix schemar input' of
Nothing => Nothing
Just (r_val, input'') => Just ((l_val, r_val), input'')
parseBySchema : (schema : Schema) -> String -> Maybe (SchemaType schema)
parseBySchema schema x = case parsePrefix schema x of
Nothing => Nothing
Just (res, "") => Just res
Just _ => Nothing
parseSchema : List String -> Maybe Schema
parseSchema ("String" :: xs)
= case xs of
[] => Just SString
_ => case parseSchema xs of
Nothing => Nothing
Just xs_sch => Just (SString .+. xs_sch)
parseSchema ("Int" :: xs)
= case xs of
[] => Just SInt
_ => case parseSchema xs of
Nothing => Nothing
Just xs_sch => Just (SInt .+. xs_sch)
parseSchema _ = Nothing
parseCommand : (schema : Schema) -> String -> String -> Maybe (Command schema)
parseCommand schema "add" rest = case parseBySchema schema rest of
Nothing => Nothing
Just restok => Just (Add restok)
parseCommand schema "get" val = case all isDigit (unpack val) of
False => Nothing
True => Just (Get (cast val))
parseCommand schema "quit" "" = Just Quit
parseCommand schema "schema" rest
= case parseSchema (words rest) of
Nothing => Nothing
Just schemaok => Just (SetSchema schemaok)
parseCommand _ _ _ = Nothing
parse : (schema : Schema) -> (input : String) -> Maybe (Command schema)
parse schema input = case span (/= ' ') input of
(cmd, args) => parseCommand schema cmd (ltrim args)
display : SchemaType schema -> String
display {schema = SString} item = show item
display {schema = SInt} item = show item
display {schema = (y .+. z)} (iteml, itemr) = display iteml ++ ", " ++
display itemr
getEntry : (pos : Integer) -> (store : DataStore) ->
Maybe (String, DataStore)
getEntry pos store
= let store_items = items store in
case integerToFin pos (size store) of
Nothing => Just ("Out of range\n", store)
Just id => Just (display (index id (items store)) ++ "\n", store)
processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input
= case parse (schema store) input of
Nothing => Just ("Invalid command\n", store)
Just (Add item) =>
Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
Just (SetSchema schema') =>
case setSchema store schema' of
Nothing => Just ("Can't update schema when entries in store\n", store)
Just store' => Just ("OK\n", store')
Just (Get pos) => getEntry pos store
Just Quit => Nothing
main : IO ()
main = replWith (MkData (SString .+. SString .+. SInt) _ []) "Command: " processInput
it can define scheme of a "database" with String and Int in runtime:
Command: schema String String Int OK Command: add "Rain Dogs" "Tom Waits" 1985 ID 0 Command: add "Fog on the Tyne" "Lindisfarne" 1971 ID 1 Command: get 1 "Fog on the Tyne", "Lindisfarne", 1971 Command: quit
I want to know if any dynamic language like ruby or python can do the same thing?In the static language,the scheme must be defined before the compile.
Thanks!
The purpose of a static type system is to reject ill-typed programs. In other words, a static type system prevents you from writing programs.
So, if you can write a program in a language with a static type system, then you can also write that same program in a language without a static type system.
Note that this is an extremely simplified explanation. I am well aware of the power of static type systems, and I love to use them. However, when it comes down to it, a static type system never enables you to write a program you couldn't otherwise write, it only prevents you from writing programs that are not well-typed.
In the static language, the scheme must be defined before the compile
This can be alleviated by something like F#'s Type Providers. Type Providers are code that runs during the compilation process and can generate type information that is not statically available in the program source text.
For example, there is a SQLProvider which can connect to a SQL database, read out its schema, and generate F# types from the schema.
But, of course, all of this still happens at compile time. The generated types will be the ones from the time you compiled the program, not when you actually connect to the database, and if the database schema changes, you have to re-run the type provider to generate new types.