More repl features (search for type, browse module, show docs, print function definition, etc.)

[michelrandahl]

More repl features

I propose we give fsharp-interactive some love by adding some more features to it.

In particular, I would love to be able to list all functions in a namespace/module, print function definitions, print docs and search for functions by type.

For reference this is what you can do in the Idris repl:

Idris> :?

Idris version 1.0
-----------------

   Command         Arguments   Purpose

   <expr>                      Evaluate an expression
   :t :type        <expr>      Check the type of an expression
   :core           <expr>      View the core language representation of a term
   :miss :missing  <name>      Show missing clauses
   :doc            <name>      Show internal documentation
   :mkdoc          <namespace> Generate IdrisDoc for namespace(s) and dependencies
   :apropos        [<package list>] <name> Search names, types, and documentation
   :s :search      [<package list>] <expr> Search for values by type
   :wc :whocalls   <name>      List the callers of some name
   :cw :callswho   <name>      List the callees of some name
   :browse         <namespace> List the contents of some namespace
   :total          <name>      Check the totality of a name
   :r :reload                  Reload current file
   :w :watch                   Watch the current file for changes
   :l :load        <filename>  Load a new file
   :!              <command>   Run a shell command
   :cd             <filename>  Change working directory
   :module         <module>    Import an extra module
   :e :edit                    Edit current file using $EDITOR or $VISUAL
   :m :metavars                Show remaining proof obligations (metavariables or holes)
   :p :prove       <hole>      Prove a metavariable
   :elab           <hole>      Build a metavariable using the elaboration shell
   :a :addproof    <name>      Add proof to source file
   :rmproof        <name>      Remove proof from proof stack
   :showproof      <name>      Show proof
   :proofs                     Show available proofs
   :x              <expr>      Execute IO actions resulting from an expression using the interpreter
   :c :compile     <filename>  Compile to an executable [codegen] <filename>
   :exec :execute  [<expr>]    Compile to an executable and run
   :dynamic        <filename>  Dynamically load a C library (similar to %dynamic)
   :dynamic                    List dynamically loaded C libraries
   :? :h :help                 Display this help text
   :set            <option>    Set an option (errorcontext, showimplicits, originalerrors, autosolve, nobanner, warnreach, evaltypes, desugarnats)
   :unset          <option>    Unset an option
   :color :colour  <option>    Turn REPL colours on or off; set a specific colour
   :consolewidth   auto|infinite|<number>Set the width of the console
   :printerdepth   [<number>]  Set the maximum pretty-printer depth (no arg for infinite)
   :q :quit                    Exit the Idris system
   :warranty                   Displays warranty information
   :let            (<top-level declaration>)...Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration
   :unlet :undefine(<name>)... Remove the listed repl definitions, or all repl definitions if no names given
   :printdef       <name>      Show the definition of a function
   :pp :pprint     <option> <number> <name>Pretty prints an Idris function in either LaTeX or HTML and for a specified width.
   :verbosity      <number>    Set verbosity level

Searching by type:

Idris> :s List (Maybe a) -> Maybe (List a)
< Prelude.Traversable.sequence : Traversable t => Applicative f => t (f a) -> f (t a)
Evaluate each computation in a structure and collect the results

Printing functions definitions:

Idris> :printdef Prelude.Traversable.sequence
sequence : Traversable t => Applicative f => t (f a) -> f (t a)
sequence = traverse id

Printing docs:

Idris> :doc Prelude.Traversable.sequence
Prelude.Traversable.sequence : Traversable t => Applicative f => t (f a) -> f (t a)
    Evaluate each computation in a structure and collect the results

    The function is Total

Browse a namespace:

Idris> :browse Prelude.Traversable
Namespaces:

Names:
  Traversable : (Type -> Type) -> Type
  for : Traversable t => Applicative f => t a -> (a -> f b) -> f (t b)
  for_ : Foldable t => Applicative f => t a -> (a -> f b) -> f ()
  sequence : Traversable t => Applicative f => t (f a) -> f (t a)
  sequence_ : Foldable t => Applicative f => t (f a) -> f ()
  traverse : Traversable t => Applicative f => (a -> f b) -> t a -> f (t b)
  traverse_ : Foldable t => Applicative f => (a -> f b) -> t a -> f ()

Pros and Cons

I think this would greatly improve the developer-user-experience across all platforms.

[dsyme]

@michelrandahl Of the list above, I think the following are of most immediate interest, and I believe we would accept good PRs for them after RFC, testing etc.:

#t :type        <expr>      Check the type of an expression
#!              <command>   Run a shell command
#color :colour  <option>    Turn REPL colours on or off; set a specific colour
#consolewidth   auto|infinite|<number>Set the width of the console

Also things that represent existing F# compiler options e.g.

#define ident

The features to search the APIs etc. feel less compelling to me since F# is almost always used with some kind of assisted editor tooling, which implement such features, and there feels like a potential for a fairly substantial bug trail for the above. But that's just my feeling.

[cloudRoutine]

#!              <command>   Run a shell command

^ this would be so useful

[dsyme]

@cloudRoutine It's certainly approved to proceed to an RFC and PR for these