REPLs with Typed Holes

by

I have made a comparison among several programming languages with REPL and typed holes (well, maybe not natively) support, including Arend, GHC Haskell, PureScript, F#, Agda, Idris, Idris2, and the experimental language for the CHM paper, cubicaltt. I have the original gist.

Note that Agda REPL is abandoned, cubicaltt is experimental, Arend REPL is not even merged into the master branch, and Idris2 is still under active development.

I made this because I was working on a REPL for Arend, in both cli and IDE, and I need others’ work in the industry as references. I hope this can be helpful to you as well.

Here’s a simple table as a summary (converted from Excel via https://thisdavej.com/copy-table-in-excel-and-paste-as-a-markdown-table):

Language Arend GHC Haskell PureScript F# Agda Idris Idris2 cubicaltt
Type system HoTT-I System F System F System F Cubical TT MLTT MLTT+QTT Cubical TT
Typed holes Builtin Builtin Builtin Hacky Builtin Builtin Builtin Builtin
Expressions Hidden Hidden Hidden Printed Evaluated Elaborated Elaborated Printed
Builtin + type Nat class Num class Semiring type int type Nat class Num class Num N/A
Startup Fast Fast Very slow Fast Fast Slow Fast Fast
Status Head Stable Stable Stable Abandoned Stable Experimental Toy
Based on Nothing Nothing Project Nothing File Nothing Nothing File
Banner × × × ×
Candidates × × × × × × ×
Syntax {?A} _A ?A N/A ?, {!!} ?A ?A ?
Named hole Optional Optional Enforced × × Enforced Optional ×
Completion × × ×
Help :? :? :? #help;; :? :? :? :h
Quit :q :q :q #quit;; :q :q :q :q

Below is my experiment.

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-18b644965
  _/ // /_/ / /  / (__  )   / __/      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

Tweet this Top

License

This work (REPLs with Typed Holes) is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

License



Create an issue to apply for commentary