CH examples

ch1.ml

(* CH examples *)

(* projection *)
let e1q1 = fun x y -> x;;

(* application twist *)
let e1q2 = fun x f -> f x;;

(* application *)
let e1q2v = fun f x -> f x;;

(* composition *)
let e1q3 = fun f g x -> g(f(x));;

let e1q3bonus = fun (f:'a -> 'b) (g:'c -> 'd) (h:'b -> 'c) : ('a -> 'd) -> fun (x:'a) : 'd -> g (h (f x));;

let e1q4 = fun f g x -> f x (g x);;

(* ignore then const from fst *)
let e2q1 = fun x ->
    let e2q1h1 = (true, 0) in (* hypothèse : on a une paire d'habitants de deux types *)
    let e2q1h1f = fst e2q1h1 in
    let e2q1h1s = snd e2q1h1 in
    if x == e2q1h1f then e2q1h1s else e2q1h1s
;;

(* version abstraite *)
let e2q1v = fun x ->
    let e2q1h1 = (`A, `B) in
    let e2q1h1f = fst e2q1h1 in
    let e2q1h1s = snd e2q1h1 in
    if x == e2q1h1f then e2q1h1s else e2q1h1s
;;

(* one-liner variant, kind of *)
let e2q1w = function |`A -> `B;;

(* version implication *)
let e2q1i = fun (x:'a * 'b) -> match x with | (a,b) -> fun (x:'a) -> b;;

(* curry or not *)
let e2q2p1 =  fun f -> fun (x,y) -> f x y;;
let e2q2p2 =  fun f -> fun x y -> f (x,y);;

(* swap two args *)
let e2q3 = fun f -> fun x y -> f y x;;

(* version réifiée *)
let e2q4 =
    let e2q4h1 = fun x -> if x == 0. then (0, false) else (1, true) in (* hypothèse *)
    let e2q4p1 = fun x -> fst (e2q4h1 x) in
    let e2q4p2 = fun x -> snd (e2q4h1 x) in
    (e2q4p1, e2q4p2)
;;

(* version abstraite *)
let e2q4v =
    let e2q4h1 = function | `A -> (`B, `C) in (* hypothèse *)
    let e2q4p1 = fun x -> fst (e2q4h1 x) in
    let e2q4p2 = fun x -> snd (e2q4h1 x) in
    (e2q4p1, e2q4p2)
;;

(* version implication *)
let e2q4i = fun (f:'a -> ('b * 'c)) ->
    let fa = fun (x:'a) -> fst (f x) in
    let fb = fun (x:'a) -> snd (f x) in
    (fa,fb);;

(* version réifiée *)
type e3t1 = A1 of int | BC1 of (bool * float) (* A v (B ^ C) *)
type e3t2 = A2 of int | B2 of bool (* A v B *)
type e3t3 = A3 of int | C3 of float (* A v C *)

let e3p1 = function
    | A1(a) -> (A2(a), A3(a))
    | BC1(b, c) -> (B2(b), C3(c))
;;

let e3p2 = function
    | (A2(a2), A3(a3)) -> A1(a2)
    | (A2(a2), C3(c3)) -> A1(a2)
    | (B2(b2), A3(a3)) -> A1(a3)
    | (B2(b2), C3(c3)) -> BC1(b2,c3)
;;

(* version abstraite *)
type e3vt1 = Av1 of [`A] | BCv1 of ([`B] * [`C])
type e3vt2 = Av2 of [`A] | Bv2 of [`B]
type e3vt3 = Av3 of [`A] | Cv3 of [`C]

let e3vp1 = function
    | Av1(a) -> (Av2(a), Av3(a))
    | BCv1(b, c) -> (Bv2(b), Cv3(c))
;;

let e3vp2 = function
    | (Av2(a2), Av3(a3)) -> Av1(a2)
    | (Av2(a2), Cv3(c3)) -> Av1(a2)
    | (Bv2(b2), Av3(a3)) -> Av1(a3)
    | (Bv2(b2), Cv3(c3)) -> BCv1(b2,c3)
;;

(* version polymorphe *)
type ('a, 'b, 'c) e3wt1 = Aw1 of 'a | BCw1 of ('b * 'c)
type ('a, 'b) e3wt2 = Aw2 of 'a | Bw2 of 'b
type ('a, 'c) e3wt3 = Aw3 of 'a | Cw3 of 'c

let e3wp1 = function
    | Aw1(a) -> (Aw2(a), Aw3(a))
    | BCw1(b, c) -> (Bw2(b), Cw3(c))
;;

let e3wp2 = function
    | (Aw2(a2), _) -> Aw1(a2)
    | (_, Aw3(a3)) -> Aw1(a3)
    | (Bw2(b2), Cw3(c3)) -> BCw1(b2,c3)
;;

(* types pour la négation *)

type empty = |
type 'a not = 'a -> empty

(* exemple 8 *)

let ex8 = fun (x:'a) -> fun(f:'a -> empty) -> f x;;
let ex8v = fun(x:'a) : 'a not not -> fun(f:'a not) -> f x;;

(* contraposition *)
(* aussi exercice 7 q.2 gauche à droite *)
let contra = fun (f:'a -> 'b) : ('b not -> 'a not) -> fun (g:'b not) -> fun (x:'a) -> g(f x);;

(* exercice 4 *)

(* shown as implications *)
let e4q1 = fun (x:'a * 'a not) : empty -> (snd x) (fst x);;
(* curried variant, in fact identical to ex8 *)
let e4q1v = fun (x:'a) (f:'a not) : empty -> f x;;

(* only shown as an implication; last step's easy w/ natural deduction,
 * and in any case one can't construct a suitable assumption for any inhabited type
 * since it would then allow to prove false by evaluating the function on one of its elements? *)
let e4q2 e = contra ex8v e;;  (* η-expansion to prevent getting a weak type *)

(* XENS 2024 Info C Q.14 *)

(* version simplifiée ; comme une implication *)
let xens2024cq14s = fun (f:'a -> 'a not) : 'a not -> fun (x:'a) -> f x x;;

(* version complète for show ; comme une implication *)
let xens2024cq14 = fun (f:(('a -> ('a not * 'b)) * (('a not * 'b) -> 'a))) : 'a not ->
    let ff = fst f in
    fun (x:'a) -> fst(ff x) x
;;

(* ex falso quodlibet (DM inf110-02.56) *)
let efqv = fun (x:empty) -> match x with _ -> .;; (* using match case refutation: the wildcard that catches any inhabitant doesn't catch anything *) (* now only valid for the actual empty type *)

(* exercice 7 q.3 droite à gauche *)
type ('a, 'b) e7t1 = A7n of 'a not | B7 of 'b

let e7q3p1  = function
    | B7(b) -> fun (x:'a) -> b
    | A7n(a) -> fun (x:'a) -> efq (e4q1v x a)
;;

(* exemple du programme *)
let ep = fun (f:'a -> 'b) : ('a * 'b not) not ->
    fun (x:'a * 'b not) ->
        let xa = fst x in
        let xb = snd x in
        xb (f xa)
;;

(* saem, one-liner implem *)
let epv = fun (f:'a -> 'b) : ('a * 'b not) not -> function | (a, bn) -> bn (f a);;

(* saem, without type annotations -> doesn't restrict 'b to be negated -> more general proposition *)
let epf = fun f -> function | (a, g) -> g (f a);;