Emulating Idris-style holes

A simple function that sort of emulates the holes feature of Idris for F#

Definition

1: 
2: 
3: 
4: 
5: 
6:

open System

type Hole = Hole

[<CompilerMessage("Incomplete hole", 130)>]
let (?) (_ : Hole) (id : string) : 'T = raise <| NotImplementedException(sprintf "Incomplete hole '%s : %O'" id typeof<'T>)

Example

 1: 
 2: 
 3: 
 4: 
 5: 
 6: 
 7: 
 8: 
 9: 
10:

let abs n =
    if n >= 0 then n
    else Hole ?TODO_Negation

// compile time warning:
// Test.fs(28,15): warning FS0130: Incomplete hole
// val abs : n:int -> int

abs 2 // successful
abs -1 // System.NotImplementedException: Incomplete hole 'TODO_Negation : System.Int32'

namespace System

Multiple items
union case Hole.Hole: Hole

--------------------
type Hole = | Hole

Full name: Script.Hole

Multiple items
type CompilerMessageAttribute =
  inherit Attribute
  new : message:string * messageNumber:int -> CompilerMessageAttribute
  member IsError : bool
  member IsHidden : bool
  member Message : string
  member MessageNumber : int
  member IsError : bool with set
  member IsHidden : bool with set

Full name: Microsoft.FSharp.Core.CompilerMessageAttribute

--------------------
new : message:string * messageNumber:int -> CompilerMessageAttribute

val id : string

Multiple items
val string : value:'T -> string

Full name: Microsoft.FSharp.Core.Operators.string

--------------------
type string = String

Full name: Microsoft.FSharp.Core.string

val raise : exn:Exception -> 'T

Full name: Microsoft.FSharp.Core.Operators.raise

Multiple items
type NotImplementedException =
inherit SystemException
new : unit -> NotImplementedException + 2 overloads

Full name: System.NotImplementedException

--------------------
NotImplementedException() : unit
NotImplementedException(message: string) : unit
NotImplementedException(message: string, inner: exn) : unit

val sprintf : format:Printf.StringFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.sprintf

val typeof<'T> : Type

Full name: Microsoft.FSharp.Core.Operators.typeof

val abs : n:int -> int

Full name: Script.abs

val n : int

Next Version Raw view Test code New version

More information

Link:	http://fssnip.net/7V5
Posted:	7 years ago
Author:	Eirik Tsarpalis
Tags:	holes , idris , type driven development