Comparison among several REPLs with goal support

repl-goal.md

REPLs with Typed Holes

This page is deprecated and superseded by https://ice1000.org/2020/05-04-ReplWithGoals.html.

Arend

λ> java -jar cli-1.3.0-full.jar -i
Arend REPL 1.3.0: https://arend-lang.github.io   :? for help
λ \open Nat
λ 1 + {?}
[GOAL] Repl:1:5: Goal
  Expected type: Nat
  In: {?}
λ :q

GHC Haskell

λ> ghci
GHCi, version 8.8.3: https://www.haskell.org/ghc/  :? for help
Prelude> 1 + _

<interactive>:1:5: error:
    • Found hole: _ :: a
      Where: ‘a’ is a rigid type variable bound by
               the inferred type of it :: Num a => a
               at <interactive>:1:1-5
    • In the second argument of ‘(+)’, namely ‘_’
      In the expression: 1 + _
      In an equation for ‘it’: it = 1 + _
    • Relevant bindings include it :: a (bound at <interactive>:1:1)
      Constraints include Num a (from <interactive>:1:1-5)
Prelude> :q
Leaving GHCi.

PureScript Spago

(Modified to remove the "[info]" stuffs and "Compiling" logs)

λ> spago repl
PSCi, version 0.13.6
Type :? for help

import Prelude

> 1 + ?A
Error found:
in module $PSCI
at :1:5 - 1:7 (line 1, column 5 - line 1, column 7)

  Hole 'A' has the inferred type

    Int

  You could substitute the hole with one of these values:

    $PSCI.it             :: Int
    Data.Bounded.bottom  :: forall a. Bounded a => a
    Data.Bounded.top     :: forall a. Bounded a => a
    Data.Semiring.one    :: forall a. Semiring a => a
    Data.Semiring.zero   :: forall a. Semiring a => a


in value declaration it

See https://github.com/purescript/documentation/blob/master/errors/HoleInferredType.md for more information,
or to contribute content related to this error.


> :q
See ya!
()

F#

λ> fsi

Microsoft (R) F# Interactive version 10.8.0.0 for F# 4.7
Copyright (c) Microsoft Corporation. All Rights Reserved.

For help type #help;;

> let __<'a> = failwith "typed hole";;
val __<'a> : obj

> 1 + __;;

  1 + __;;
  ----^^

stdin(2,5): error FS0001: The type 'obj' does not match the type 'int'

> #quit;;

Agda

λ> cat A.agda
{-# OPTIONS --allow-unsolved-metas #-}
open import Agda.Builtin.Nat
λ> agda -I A.agda
                 _
   ____         | |
  / __ \        | |
 | |__| |___  __| | ___
 |  __  / _ \/ _  |/ __\     Agda Interactive
 | |  |/ /_\ \/_| / /_| \
 |_|  |\___  /____\_____/    Type :? for help.
        __/ /
        \__/

The interactive mode is no longer under active development. Use at your own risk.
Main> 1 + ?
suc ?0
Main> :metas
?0 : Nat
Main> :q

Idris

λ> idris
     ____    __     _
    /  _/___/ /____(_)____
    / // __  / ___/ / ___/     Version 1.3.2-git:0417c53fb
  _/ // /_/ / /  / (__  )      https://www.idris-lang.org/
 /___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Idris> 1 + ?A
prim__addBigInt 1 ?A : Integer
Holes: A
Idris> :q
Bye bye

Idris 2

λ> idris2
     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.1.0-819c9d7af
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main> 1 + ?A
prim__add_Integer 1 ?A
Main> :q
Bye for now!

cubicaltt

(Modified to remove the "Parsed successfully" and "Checking" logs)

λ> cubical nat.ctt
cubical, version: 1.0  (:h for help)

Loading "nat.ctt"
Warning: the following definitions were shadowed [retIsContr]
File loaded.
> add (suc zero) ?

Hole at (1,16) in :

--------------------------------------------------------------------------------
nat

EVAL: add (suc zero) ?
> :q

Can you do a 1 + hole example and show the quit command?

FYI https://ice1000.org/2020/05-04-ReplWithGoals.html

Unfortunately + is overloaded (java style method overloading) which causes the typechecker to fail to disambiguate:

scala> 1 + __a
         ^
       error: ambiguous reference to overloaded definition,
       both method + in class Int of type (x: Char)Int
       and  method + in class Int of type (x: Byte)Int
       match argument types (Nothing)

Manually giving a type signature to help the typechecker will make the compiler plugin to cease functioning for some reason.

Is there a way to make the type explicit?

Also, this error message actually tells you the type of the hole

Nothing is the bottom type, so it didn't actually tell me anything 🤣

scala> 1 + (__a : Int)
scala.NotImplementedError: an implementation is missing
  at scala.Predef$.$qmark$qmark$qmark(Predef.scala:347)
  ... 36 elided

NotImplementedError is a runtime error caused by evaluating a hole.

Manually giving a type signature to help the typechecker will make the compiler plugin to cease functioning for some reason.

Scala bad

true