1

REPLs with Typed Holes

 3 years ago
source link: https://ice1000.org/2020/05-04-ReplWithGoals.html
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.

REPLs with Typed Holes

2020, May 4 by Tesla Ice Zhang

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

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

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

report

Recommend

About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK