3 people like it.

# Seemingly impossible program defines equality between arbitrary functions

It is well known that it is impossible to define equality between arbitrary functions. However, there is a large class of functions for which we can determine equality, and itâ€™s strange and surprising. We explore this idea using F# code translated from the Swift programming language.

 ``` 1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 20: 21: 22: 23: 24: 25: 26: 27: 28: 29: 30: 31: 32: 33: 34: 35: 36: 37: 38: 39: 40: 41: 42: 43: 44: 45: 46: 47: 48: 49: 50: 51: 52: 53: 54: 55: 56: 57: 58: 59: 60: 61: 62: 63: 64: 65: 66: 67: 68: 69: 70: 71: 72: 73: 74: 75: 76: 77: 78: 79: 80: 81: 82: 83: 84: 85: 86: 87: 88: 89: 90: 91: 92: 93: 94: ``` ``````// https://www.fewbutripe.com/2018/12/05/seemingly-impossible.html type Bit = | Zero = 0 | One = 1 /// An infinite sequence of bits. type BitSequence = { /// Answers the bit at the given index. Article calls this "atIndex". Item : uint32 -> Bit } [] [] module BitSequence = /// Creates a bit sequence with the given lookup function. let create f = { Item = f } /// Dumps the beginning of the given sequence to the console. let dump (seq : BitSequence) = [0u .. 10u] |> Seq.iter (fun i -> printfn "%d: %A" i seq.[i]) /// Prepends the given bit to the given lazy sequence. let (++) bit (lseq : Lazy) = create (fun i -> if i = 0u then bit else lseq.Value.[i - 1u]) // don't reify the given sequence until we have to /// Finds a sequence for which the given predicate is true. /// Warning: answers garbage sequence if no such sequence exists. let rec find (pred : BitSequence -> bool) = let zeroPred seq = pred (Bit.Zero ++ lazy seq) if exists zeroPred then Bit.Zero ++ lazy (find zeroPred) else let onePred seq = pred (Bit.One ++ lazy seq) Bit.One ++ lazy (find onePred) /// Is there a sequence for which the given predicate is true? Article calls this "anySatisfy". and exists pred = let lseq = lazy (find pred) let seq = create (fun i -> lseq.Value.[i]) pred seq /// Do all sequences satisfy the given predicate? Article calls this "allSatisfy". and forall pred = pred >> not |> exists |> not /// Equality of functions that have BitSequence as their domains. let (==) (f1 : BitSequence -> 'a) (f2 : BitSequence -> 'a) = forall (fun seq -> f1 seq = f2 seq) let oneOnFirstFiveEvens () = let seq = BitSequence.find (fun seq -> seq.[0u] = Bit.One && seq.[2u] = Bit.One && seq.[4u] = Bit.One && seq.[6u] = Bit.One && seq.[8u] = Bit.One) BitSequence.dump seq let equality () = let f (seq : BitSequence) = int seq.[1u] * int seq.[2u] let g (seq : BitSequence) = int seq.[1u] + int seq.[2u] printfn "f = f: %A" (f == f) printfn "g = g: %A" (g == g) printfn "f = g: %A" (f == g) let h (seq : BitSequence) = match seq.[1u], seq.[2u] with | Bit.One, Bit.One -> 1 | _ -> 0 printfn "f = h: %A" (f == h) printfn "g = h: %A" (g == h) let k (seq : BitSequence) = ((int seq.[1u] + int seq.[2u] + 908) % 6) / 4 printfn "f = k: %A" (f == k) printfn "g = k: %A" (g == k) printfn "h = k: %A" (h == k) [] let main argv = oneOnFirstFiveEvens () printfn "" equality () 0 ``````
Bit.Zero: Bit = 0
Bit.One: Bit = 1
type BitSequence =
{Item: uint32 -> Bit;}

Full name: Script.BitSequence

An infinite sequence of bits.
BitSequence.Item: uint32 -> Bit

Answers the bit at the given index. Article calls this "atIndex".
Multiple items
val uint32 : value:'T -> uint32 (requires member op_Explicit)

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

--------------------
type uint32 = System.UInt32

Full name: Microsoft.FSharp.Core.uint32
type Bit =
| Zero = 0
| One = 1

Full name: Script.Bit
Multiple items
type AutoOpenAttribute =
inherit Attribute
new : unit -> AutoOpenAttribute
new : path:string -> AutoOpenAttribute
member Path : string

Full name: Microsoft.FSharp.Core.AutoOpenAttribute

--------------------
new : unit -> AutoOpenAttribute
new : path:string -> AutoOpenAttribute
Multiple items
type CompilationRepresentationAttribute =
inherit Attribute
new : flags:CompilationRepresentationFlags -> CompilationRepresentationAttribute
member Flags : CompilationRepresentationFlags

Full name: Microsoft.FSharp.Core.CompilationRepresentationAttribute

--------------------
new : flags:CompilationRepresentationFlags -> CompilationRepresentationAttribute
type CompilationRepresentationFlags =
| None = 0
| Static = 1
| Instance = 2
| ModuleSuffix = 4
| UseNullAsTrueValue = 8
| Event = 16

Full name: Microsoft.FSharp.Core.CompilationRepresentationFlags
CompilationRepresentationFlags.ModuleSuffix: CompilationRepresentationFlags = 4
val create : f:(uint32 -> Bit) -> BitSequence

Full name: Script.BitSequenceModule.create

Creates a bit sequence with the given lookup function.
val f : (uint32 -> Bit)
val dump : seq:BitSequence -> unit

Full name: Script.BitSequenceModule.dump

Dumps the beginning of the given sequence to the console.
Multiple items
val seq : BitSequence

--------------------
type seq<'T> = System.Collections.Generic.IEnumerable<'T>

Full name: Microsoft.FSharp.Collections.seq<_>
module Seq

from Microsoft.FSharp.Collections
val iter : action:('T -> unit) -> source:seq<'T> -> unit

Full name: Microsoft.FSharp.Collections.Seq.iter
val i : uint32
val printfn : format:Printf.TextWriterFormat<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.printfn
val bit : Bit
val lseq : Lazy<BitSequence>
Multiple items
active recognizer Lazy: Lazy<'T> -> 'T

Full name: Microsoft.FSharp.Core.ExtraTopLevelOperators.( |Lazy| )

--------------------
type Lazy<'T> = System.Lazy<'T>

Full name: Microsoft.FSharp.Control.Lazy<_>
property System.Lazy.Value: BitSequence
val find : pred:(BitSequence -> bool) -> BitSequence

Full name: Script.BitSequenceModule.find

Finds a sequence for which the given predicate is true.
Warning: answers garbage sequence if no such sequence exists.
val pred : (BitSequence -> bool)
type bool = System.Boolean

Full name: Microsoft.FSharp.Core.bool
val zeroPred : (BitSequence -> bool)
val exists : pred:(BitSequence -> bool) -> bool

Full name: Script.BitSequenceModule.exists

Is there a sequence for which the given predicate is true? Article calls this "anySatisfy".
val onePred : (BitSequence -> bool)
val forall : pred:(BitSequence -> bool) -> bool

Full name: Script.BitSequenceModule.forall

Do all sequences satisfy the given predicate? Article calls this "allSatisfy".
val not : value:bool -> bool

Full name: Microsoft.FSharp.Core.Operators.not
val f1 : (BitSequence -> 'a) (requires equality)
val f2 : (BitSequence -> 'a) (requires equality)
val oneOnFirstFiveEvens : unit -> unit

Full name: Script.oneOnFirstFiveEvens
Multiple items
module BitSequence

from Script

--------------------
type BitSequence =
{Item: uint32 -> Bit;}

Full name: Script.BitSequence

An infinite sequence of bits.
val equality : unit -> unit

Full name: Script.equality
val f : (BitSequence -> int)
Multiple items
val int : value:'T -> int (requires member op_Explicit)

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

--------------------
type int = int32

Full name: Microsoft.FSharp.Core.int

--------------------
type int<'Measure> = int

Full name: Microsoft.FSharp.Core.int<_>
val g : (BitSequence -> int)
val h : (BitSequence -> int)
val k : (BitSequence -> int)
Multiple items
type EntryPointAttribute =
inherit Attribute
new : unit -> EntryPointAttribute

Full name: Microsoft.FSharp.Core.EntryPointAttribute

--------------------
new : unit -> EntryPointAttribute
val main : argv:string [] -> int

Full name: Script.main
val argv : string []