Equality type

Weak Equality type, useful for various GADT encodings.

 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:

// Equality without Leibniz's law
module Eq = 

    type Eq<'A, 'B> = private Refl of ('A -> 'B) * ('B -> 'A)
    
    let refl<'A> () : Eq<'A, 'A> = Refl (id, id)
    let sym : Eq<'A, 'B> -> Eq<'B, 'A> = fun (Refl (f, g)) -> Refl (g, f)
    let trans : Eq<'A, 'B> -> Eq<'B, 'C> -> Eq<'A, 'C> = 
        fun (Refl (f, g)) (Refl (h, k)) -> Refl (f >> h, k >> g)
    let cast : Eq<'A, 'B> -> 'A -> 'B = fun (Refl (f, _)) -> f

// Example: http://okmij.org/ftp/ML/GADT.ml
open Eq

type NodeLink = NodeLink
type NodeNoLink = NodeNoLink

type Node<'T> =
   | Text of string
   | Bold of Node<'T> list
   | Href of Eq<NodeLink, 'T> * string
   | Mref of Eq<NodeLink, 'T> * string * Node<NodeNoLink> list

let text txt = Text txt
let bold seq = Bold seq;;

let href lnk = Href (refl (), lnk)
let mref lnk seq = Mref (refl (), lnk, seq)

let test1 = bold [text "text1"; text "text2"]
let test2 = bold [text "text1"; href "link1"]

let test3 = mref "link2" [test1; test1]
let test4 = bold [text "text3"; test3]

// Type errors
// let test31 = mref "link2" [test1; test2]
// let test41 = mref "link3" [test1; test4]

let rec capnode<'T> : Node<'T> -> Node<'T> =  
 function 
   | Text x        -> Text (x.ToUpper())
   | Bold x        -> Bold (List.map capnode x)
   | Href (eq,x)   -> Href (eq, x.ToUpper())
   | Mref (eq,l,x) -> Mref (eq, l, List.map capnode x)


let test1c = capnode test1
let test3c = capnode test3
let test4c = capnode test4

type Eq<'A,'B> = private | Refl of ('A -> 'B) * ('B -> 'A)

Full name: Script.Eq.Eq<_,_>

union case Eq.Refl: ('A -> 'B) * ('B -> 'A) -> Eq<'A,'B>

val refl : unit -> Eq<'A,'A>

Full name: Script.Eq.refl

val id : x:'T -> 'T

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

val sym : Eq<'A,'B> -> Eq<'B,'A>

Full name: Script.Eq.sym

val f : ('A -> 'B)

val g : ('B -> 'A)

val trans : Eq<'A,'B> -> Eq<'B,'C> -> Eq<'A,'C>

Full name: Script.Eq.trans

val h : ('B -> 'C)

val k : ('C -> 'B)

val cast : Eq<'A,'B> -> ('A -> 'B)

Full name: Script.Eq.cast

module Eq

from Script

Multiple items
union case NodeLink.NodeLink: NodeLink

--------------------
type NodeLink = | NodeLink

Full name: Script.NodeLink

Multiple items
union case NodeNoLink.NodeNoLink: NodeNoLink

--------------------
type NodeNoLink = | NodeNoLink

Full name: Script.NodeNoLink

type Node<'T> =
  | Text of string
  | Bold of Node<'T> list
  | Href of Eq<NodeLink,'T> * string
  | Mref of Eq<NodeLink,'T> * string * Node<NodeNoLink> list

Full name: Script.Node<_>

union case Node.Text: string -> Node<'T>

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

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

--------------------
type string = System.String

Full name: Microsoft.FSharp.Core.string

union case Node.Bold: Node<'T> list -> Node<'T>

type 'T list = List<'T>

Full name: Microsoft.FSharp.Collections.list<_>

union case Node.Href: Eq<NodeLink,'T> * string -> Node<'T>

Multiple items
module Eq

from Script

--------------------
type Eq<'A,'B> = private | Refl of ('A -> 'B) * ('B -> 'A)

Full name: Script.Eq.Eq<_,_>

union case Node.Mref: Eq<NodeLink,'T> * string * Node<NodeNoLink> list -> Node<'T>

val text : txt:string -> Node<'a>

Full name: Script.text

val txt : string

val bold : seq:Node<'a> list -> Node<'a>

Full name: Script.bold

Multiple items
val seq : Node<'a> list

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

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

val href : lnk:string -> Node<NodeLink>

Full name: Script.href

val lnk : string

val mref : lnk:string -> seq:Node<NodeNoLink> list -> Node<NodeLink>

Full name: Script.mref

Multiple items
val seq : Node<NodeNoLink> list

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

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

val test1 : Node<NodeNoLink>

Full name: Script.test1

val test2 : Node<NodeLink>

Full name: Script.test2

val test3 : Node<NodeLink>

Full name: Script.test3

val test4 : Node<NodeLink>

Full name: Script.test4

val capnode : _arg1:Node<'T> -> Node<'T>

Full name: Script.capnode

val x : string

System.String.ToUpper() : string
System.String.ToUpper(culture: System.Globalization.CultureInfo) : string

val x : Node<'T> list

Multiple items
module List

from Microsoft.FSharp.Collections

--------------------
type List<'T> =
  | ( [] )
  | ( :: ) of Head: 'T * Tail: 'T list
  interface IEnumerable
  interface IEnumerable<'T>
  member GetSlice : startIndex:int option * endIndex:int option -> 'T list
  member Head : 'T
  member IsEmpty : bool
  member Item : index:int -> 'T with get
  member Length : int
  member Tail : 'T list
  static member Cons : head:'T * tail:'T list -> 'T list
  static member Empty : 'T list

Full name: Microsoft.FSharp.Collections.List<_>

val map : mapping:('T -> 'U) -> list:'T list -> 'U list

Full name: Microsoft.FSharp.Collections.List.map

val eq : Eq<NodeLink,'T>

val l : string

val x : Node<NodeNoLink> list

val test1c : Node<NodeNoLink>

Full name: Script.test1c

val test3c : Node<NodeLink>

Full name: Script.test3c

val test4c : Node<NodeLink>

Full name: Script.test4c

Raw view Test code New version

More information

Link:	http://fssnip.net/7Rp
Posted:	7 years ago
Author:	Nick Palladinos
Tags:	equality type