Skip to content

Instantly share code, notes, and snippets.

@ice1000

ice1000/repl-goal.md

Last active May 6, 2020
Embed
What would you like to do?
Comparison among several REPLs with goal support

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
@poscat0x04

This comment has been minimized.

Copy link

@poscat0x04 poscat0x04 commented May 5, 2020

Scala w/ scala-typed-holes:

sbt:help> console
[info] Starting scala interpreter...
Welcome to Scala 2.13.1 (OpenJDK 64-Bit Server VM, Java 1.8.0_222).
Type in expressions for evaluation. Or try :help.

scala> def a[T](x: T): T = ???
                           ^
       warning: 
       Found hole with type: T
       Relevant bindings include
         x: T (bound at <console>:1:10)

a: [T](x: T)T

scala> :q
@ice1000

This comment has been minimized.

Copy link
Owner Author

@ice1000 ice1000 commented May 5, 2020

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

@ice1000

This comment has been minimized.

Copy link
Owner Author

@ice1000 ice1000 commented May 5, 2020

@poscat0x04

This comment has been minimized.

Copy link

@poscat0x04 poscat0x04 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

This comment has been minimized.

Copy link
Owner Author

@ice1000 ice1000 commented May 5, 2020

Is there a way to make the type explicit?

@ice1000

This comment has been minimized.

Copy link
Owner Author

@ice1000 ice1000 commented May 5, 2020

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

@poscat0x04

This comment has been minimized.

Copy link

@poscat0x04 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.

@ice1000

This comment has been minimized.

Copy link
Owner Author

@ice1000 ice1000 commented May 5, 2020

Scala bad

@poscat0x04

This comment has been minimized.

Copy link

@poscat0x04 poscat0x04 commented May 6, 2020

true

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.