15 people like it.

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: 
7: 
8: 
9: 
open System

type Hole = Hole

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

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 sprintf : format:Printf.StringFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.sprintf
val typeof<'T> : Type

Full name: Microsoft.FSharp.Core.Operators.typeof
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 raise : exn:Exception -> 'T

Full name: Microsoft.FSharp.Core.Operators.raise
val abs : n:int -> int

Full name: Script.abs
val n : int

More information

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