Type/identifier search in the repl

[brendanzab]

Would be super groovy if you could search for functions in-scope with :s. Here is what you can do in the Idris repl:

Idris> :search Monad f => f a -> f b -> f a
< Prelude.Applicative.(*>) : Applicative f => f a -> f b -> f b

< Prelude.Applicative.(<*) : Applicative f => f a -> f b -> f a

> Prelude.List.intercalate : List a -> List (List a) -> List a
Given a separator list and some more lists, produce a new list
by placing the separator between each of the lists.

> Prelude.List.(++) : List a -> List a -> List a
Append two lists

> Language.Reflection.Elab.Prim__Try : Elab a ->
                                       Elab a -> Elab a

> Prelude.List.(\\) : Eq a => List a -> List a -> List a
The \\ function is list difference (non-associative). In the
result of xs \\ ys, the first occurrence of each element of ys
in turn (if any) has been removed from xs, e.g.,

> Prelude.List.merge : Ord a => List a -> List a -> List a
Merge two sorted lists using the default ordering for the type
of their elements.

> Prelude.List.union : Eq a => List a -> List a -> List a
Compute the union of two lists according to their Eq
implementation.

> Prelude.while : IO' l Bool -> IO' l () -> IO' l ()
Loop while some test is true

[Marwes]

That would be super cool! I suppose that how complicated this is to implement depends wholly on how good the search should be so starting with a simple search to see what may parts may be needed should be a good plan. Just of the top of my head I am guessing that the parser crate needs to expose a way to just parse type and a the vm crate needs a visitor to visit all globally reachable variables and fields.

A good place to start would be to look at the :i and :k commands to see what can be extracted and generalized from them.

[brendanzab]

:t and :k are also really basic - would be nice if they could take arbitrary expressions

[Marwes]

:t does take an expression though, do you mean :i? I am not sure what the behaviour should be for :i in that case (what is the info of 1 + 1?).

For :k it could be nice if it could take any type and print its kind (so :k Option a in addition to :k Option a)

[brendanzab]

I get super confuzzled by the repl >_<

λ cargo run -- -i
     Running `target/debug/repl -i`
gluon (:h for help, :q to quit)
> :k Option
Binding `` is not defined
> :k Int
Binding `` is not defined
> :k 1
Binding `` is not defined
> :t Some
<repl>:Line: 1, Column: 1: Undefined variable `Some`
Some
^~~~

> :t Some 1
<repl>:Line: 1, Column: 1: Undefined variable `Some`
Some 1
^~~~

> :l std/prelude.glu
prelude.:Line: 1, Column: 1: Type 'Eq' has been already been defined in this module
let { Bool, Option, Result, Ordering } = import "std/types.glu"
^~
prelude.:Line: 92, Column: 5: Expected the following types to be equal
Expected: prelude..Eq ()
Found: std.prelude.Eq ()
1 errors were found during unification:
Types do not match:
    Expected: prelude..Eq
    Found: std.prelude.Eq
let eq_Unit : Eq () = {
    ^~~~~~~
prelude.:Line: 96, Column: 5: Expected the following types to be equal
Expected: prelude..Eq std.types.Bool
Found: std.prelude.Eq (| False | True)
1 errors were found during unification:
Types do not match:
    Expected: prelude..Eq
    Found: std.prelude.Eq
let eq_Bool : Eq Bool = {

....

(and on-and-on)

[Marwes]

Definitely some bugs/things I haven't implemented there.

> :k Option
Binding `` is not defined

Try :k std.prelude.Option. Normally Option is imported through injecting part of the prelude but since its not actually an expression that is passed to :k it has no knowledge of it. The error message should be better though.

> :k Int
Binding `` is not defined

Primitive types aren't handled, should be a pretty easy fix though

> :k 1
Binding `` is not defined

Running it in ghci gives:

Prelude> :k 1

<interactive>:1:1:
    Illegal literal in type (use DataKinds to enable): 1

Any actual expression should give a kind of just Type. I guess the DataKinds extension may make it useful.

> :t Some
<repl>:Line: 1, Column: 1: Undefined variable `Some`
Some
^~~~
> :t Some 1
<repl>:Line: 1, Column: 1: Undefined variable `Some`
Some 1
^~~~

The implicit prelude is disabled for :t but it probably shouldn't be, not sure why I disbled it...

> :l std/prelude.glu
prelude.:Line: 1, Column: 1: Type 'Eq' has been already been defined in this module
let { Bool, Option, Result, Ordering } = import "std/types.glu"
^~
prelude.:Line: 92, Column: 5: Expected the following types to be equal
Expected: prelude..Eq ()
Found: std.prelude.Eq ()
1 errors were found during unification:
Types do not match:
    Expected: prelude..Eq
    Found: std.prelude.Eq
let eq_Unit : Eq () = {
    ^~~~~~~
prelude.:Line: 96, Column: 5: Expected the following types to be equal
Expected: prelude..Eq std.types.Bool
Found: std.prelude.Eq (| False | True)
1 errors were found during unification:
Types do not match:
    Expected: prelude..Eq
    Found: std.prelude.Eq
let eq_Bool : Eq Bool = {

This is the weirdest one. I think that the prelude is already loaded but it is given a different name when using :l (so it is not taken from cache) and then all sorts of conflicts occur.

[brendanzab]

Gotta love this!

> :k std.prelude.Option Int
Type `{ Bool = | False | True Ordering = | LT | EQ | GT Option a = | None | Some a Result e t = | Err e | Ok t List a = | Nil | Cons a (std.prelude.List a) Monoid m = { append: m -> m -> m, empty: m } Eq a = { ==: a -> a -> std.types.Bool } Ord a = { eq: std.prelude.Eq a, compare: a -> a -> std.types.Ordering } Category cat = { id: cat a a, compose: cat b c -> cat a b -> cat a c } Functor f = { map: (a -> b) -> f a -> f b } Applicative f = { functor: std.prelude.Functor f, apply: f (a -> b) -> f a -> f b, pure: a -> f a } Alternative f = { applicative: std.prelude.Applicative f, or: f a -> f a -> f a, empty: f a } Monad m = { applicative: std.prelude.Applicative m, flat_map: (a -> m b) -> m a -> m b } Num a = { ord: std.prelude.Ord a, +: a -> a -> a, -: a -> a -> a, *: a -> a -> a, /: a -> a -> a, negate: a -> a } Show a = { show: a -> String }, not: | False | True -> std.types.Bool, foldl: (t0 -> t1 -> t0) -> t0 -> std.prelude.List t1 -> t0, foldr: (t2 -> t3 -> t3) -> t3 -> std.prelude.List t2 -> t3, make_Monoid: std.prelude.Monoid t4 -> { append: t5 -> t5 -> t5, empty: t6, <>: t7 -> t7 -> t7 }, monoid_Function: std.prelude.Monoid t8 -> std.prelude.Monoid (t9 -> t8), monoid_List: std.prelude.Monoid (std.prelude.List t10), monoid_Option: std.prelude.Monoid t11 -> std.prelude.Monoid (std.types.Option t11), monoid_Int_Add: std.prelude.Monoid Int, monoid_Int_Mul: std.prelude.Monoid Int, monoid_Float_Add: std.prelude.Monoid Float, monoid_Float_Mul: std.prelude.Monoid Float, eq_Unit: std.prelude.Eq (), eq_Bool: std.prelude.Eq std.types.Bool, eq_List: std.prelude.Eq t12 -> std.prelude.Eq (std.prelude.List t12), eq_Option: std.prelude.Eq t13 -> std.prelude.Eq (std.types.Option t13), eq_Result: std.prelude.Eq t14 -> std.prelude.Eq t15 -> std.prelude.Eq (std.types.Result t14 t15), eq_Float: std.prelude.Eq Float, eq_Int: std.prelude.Eq Int, eq_Char: std.prelude.Eq Char, make_Ord: std.prelude.Ord t16 -> { eq: std.prelude.Eq t16, compare: t16 -> t16 -> std.types.Ordering, <=: t16 -> t16 -> std.types.Bool, <: t16 -> t16 -> std.types.Bool, >: t16 -> t16 -> std.types.Bool, >=: t16 -> t16 -> std.types.Bool }, ord_Unit: std.prelude.Ord (), ord_Bool: std.prelude.Ord std.types.Bool, ord_Option: std.prelude.Ord t17 -> std.prelude.Ord (std.types.Option t17), ord_Result: std.prelude.Ord t18 -> std.prelude.Ord t19 -> std.prelude.Ord (std.types.Result t18 t19), ord_Float: std.prelude.Ord Float, ord_Int: std.prelude.Ord Int, ord_Char: std.prelude.Ord Char, make_Category: std.prelude.Category t20 -> { id: t22 t21 t21, compose: t25 t23 t24 -> t25 t26 t23 -> t25 t26 t24, <<: t29 t27 t28 -> t29 t30 t27 -> t29 t30 t28, >>: t33 t31 t32 -> t33 t32 t34 -> t33 t31 t34 }, category_Function: std.prelude.Category ->, functor_Option: std.prelude.Functor std.types.Option, functor_Result: std.prelude.Functor (std.types.Result t35), functor_List: std.prelude.Functor std.prelude.List, functor_IO: std.prelude.Functor IO, make_Applicative: std.prelude.Applicative t36 -> { functor: std.prelude.Functor t37, apply: t40 (t38 -> t39) -> t40 t38 -> t40 t39, pure: t41 -> t42 t41, <*>: t45 (t43 -> t44) -> t45 t43 -> t45 t44, <*: t47 t46 -> t47 t48 -> t47 t46, *>: t50 t49 -> t50 t51 -> t50 t51, map2: (t52 -> t53 -> t54) -> t55 t52 -> t55 t53 -> t55 t54, map3: (t56 -> t57 -> t58 -> t59) -> t60 t56 -> t60 t57 -> t60 t58 -> t60 t59 }, applicative_Option: std.prelude.Applicative std.types.Option, applicative_Result: std.prelude.Applicative (std.types.Result t61), applicative_List: std.prelude.Applicative std.prelude.List, applicative_IO: std.prelude.Applicative IO, make_Alternative: std.prelude.Alternative t62 -> { applicative: std.prelude.Applicative t63, or: t65 t64 -> t65 t64 -> t65 t64, empty: t67 t66, <|>: t69 t68 -> t69 t68 -> t69 t68, many: t71 t70 -> t71 (std.prelude.List t70), some: t73 t72 -> t73 (std.prelude.List t72) }, alternative_Option: std.prelude.Alternative std.types.Option, alternative_List: std.prelude.Alternative std.prelude.List, make_Monad: std.prelude.Monad t74 -> { applicative: std.prelude.Applicative t75, flat_map: (t76 -> t78 t77) -> t78 t76 -> t78 t77, =<<: (t79 -> t81 t80) -> t81 t79 -> t81 t80, >>=: t83 t82 -> (t82 -> t83 t84) -> t83 t84, join: t86 (t86 t85) -> t86 t85, forM_: std.prelude.List t87 -> (t87 -> t89 t88) -> t89 () }, monad_Option: std.prelude.Monad std.types.Option, monad_List: std.prelude.Monad std.prelude.List, monad_IO: std.prelude.Monad IO, num_Int: std.prelude.Num Int, num_Float: std.prelude.Num Float, id: t90 -> t90, const: t91 -> t92 -> t91, flip: (t93 -> t94 -> t95) -> t94 -> t93 -> t95, <|: (t96 -> t97) -> t96 -> t97, |>: t98 -> (t98 -> t99) -> t99, <<: (t100 -> t101) -> (t102 -> t100) -> t102 -> t101, >>: (t103 -> t104) -> (t104 -> t105) -> t103 -> t105, show_Unit: std.prelude.Show (), show_Bool: std.prelude.Show std.types.Bool, show_Int: std.prelude.Show Int, show_Float: std.prelude.Show Float, show_List: std.prelude.Show t106 -> std.prelude.Show (std.prelude.List t106), show_Option: std.prelude.Show t107 -> std.prelude.Show (std.types.Option t107), show_Result: std.prelude.Show t108 -> std.prelude.Show t109 -> std.prelude.Show (std.types.Result t108 t109) }` does not have the field `Option Int`

(yes, I know it isn't meant to work on type expressions 😉 )

[brendanzab]

And yes, I understand that is more a problem with structural typing...

[Marwes]

That reminds me to add an issue for printing large types #72