Instantly share code, notes, and snippets.

# ice1000/repl-goal.md

Last active May 6, 2020 01:14
Show Gist options
• Save ice1000/c20426a218c7b08374e71985734a7b39 to your computer and use it in GitHub Desktop.
Comparison among several REPLs with goal support

# REPLs with Typed Holes

## 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
``````

``````λ> 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

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

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
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
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)

Warning: the following definitions were shadowed [retIsContr]

Hole at (1,16) in :

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

> :q
``````

### ice1000 commented May 5, 2020

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

### ice1000 commented May 5, 2020

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.

### ice1000 commented May 5, 2020

Is there a way to make the type explicit?

### ice1000 commented May 5, 2020

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

### poscat0x04 commented May 5, 2020

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.