mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
179 lines
3.0 KiB
Plaintext
179 lines
3.0 KiB
Plaintext
(* ****** ****** *)
|
|
//
|
|
// HX-2014-01
|
|
// Yoneda Lemma:
|
|
// The hardest "trivial" theorem :)
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
#include
|
|
"share/atspre_staload.hats"
|
|
//
|
|
(* ****** ****** *)
|
|
|
|
staload
|
|
"libats/ML/SATS/basis.sats"
|
|
staload
|
|
"libats/ML/SATS/list0.sats"
|
|
staload
|
|
"libats/ML/SATS/option0.sats"
|
|
|
|
(* ****** ****** *)
|
|
|
|
staload _ = "libats/ML/DATS/list0.dats"
|
|
staload _ = "libats/ML/DATS/option0.dats"
|
|
|
|
(* ****** ****** *)
|
|
|
|
sortdef ftype = type -> type
|
|
|
|
(* ****** ****** *)
|
|
|
|
infixr (->) ->>
|
|
typedef ->> (a:type, b:type) = a -<cloref1> b
|
|
|
|
(* ****** ****** *)
|
|
|
|
typedef
|
|
functor(F:ftype) =
|
|
{a,b:type} (a ->> b) ->> F(a) ->> F(b)
|
|
|
|
(* ****** ****** *)
|
|
|
|
typedef
|
|
list0 (a:type) = list0 (a)
|
|
extern
|
|
val functor_list0 : functor (list0)
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
functor_list0{a,b}
|
|
(f) = lam xs => list0_map<a><b> (xs, f)
|
|
|
|
(* ****** ****** *)
|
|
|
|
typedef
|
|
option0 (a:type) = option0 (a)
|
|
extern
|
|
val functor_option0 : functor (option0)
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
functor_option0{a,b}
|
|
(f) = lam opt => option0_map<a><b> (opt, f)
|
|
|
|
(* ****** ****** *)
|
|
|
|
extern
|
|
val functor_homres
|
|
: {c:type} functor (lam(r:type) => c ->> r)
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
functor_homres{c}{a,b} (f) = lam (r) => lam (x) => f (r(x))
|
|
|
|
(* ****** ****** *)
|
|
//
|
|
extern
|
|
fun Yoneda_phi : {F:ftype}functor(F) ->
|
|
{a:type}F(a) ->> ({r:type}(a ->> r) ->> F(r))
|
|
extern
|
|
fun Yoneda_psi : {F:ftype}functor(F) ->
|
|
{a:type}({r:type}(a ->> r) ->> F(r)) ->> F(a)
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
implement
|
|
Yoneda_phi
|
|
(ftor) = lam(fx) => lam (m) => ftor(m)(fx)
|
|
//
|
|
implement
|
|
Yoneda_psi (ftor) = lam(mf) => mf(lam x => x)
|
|
//
|
|
(* ****** ****** *)
|
|
|
|
(*
|
|
|
|
(* ****** ****** *)
|
|
//
|
|
// HX-2014-01-05:
|
|
// Another version based on Natural Transformation
|
|
//
|
|
(* ****** ****** *)
|
|
|
|
typedef
|
|
natrans(F:ftype, G:ftype) = {x:type} (F(x) ->> G(x))
|
|
|
|
(* ****** ****** *)
|
|
//
|
|
extern
|
|
fun Yoneda_phi_nat : {F:ftype}functor(F) ->
|
|
{a:type} F(a) ->> natrans(lam (r:type) => (a ->> r), F)
|
|
extern
|
|
fun Yoneda_psi_nat : {F:ftype}functor(F) ->
|
|
{a:type} natrans(lam (r:type) => (a ->> r), F) ->> F(a)
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
implement
|
|
Yoneda_phi_nat
|
|
(ftor) = lam(fx) => lam (m) => ftor(m)(fx)
|
|
//
|
|
implement
|
|
Yoneda_psi_nat (ftor) = lam(mf) => mf(lam x => x)
|
|
//
|
|
(* ****** ****** *)
|
|
|
|
*)
|
|
|
|
(* ****** ****** *)
|
|
|
|
datatype bool = True | False // boxed boolean
|
|
|
|
(* ****** ****** *)
|
|
//
|
|
fun bool2string
|
|
(x:bool): string =
|
|
(
|
|
case+ x of True() => "True" | False() => "False"
|
|
)
|
|
//
|
|
implement
|
|
fprint_val<bool> (out, x) = fprint (out, bool2string(x))
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
val myboolist0 =
|
|
$list_t{bool}(True, False, True, False, False)
|
|
val myboolist0 = g0ofg1_list (myboolist0)
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
extern
|
|
val Yoneda_bool_list0 : {r:type} (bool ->> r) ->> list0(r)
|
|
//
|
|
implement
|
|
Yoneda_bool_list0 =
|
|
Yoneda_phi(functor_list0){bool}(myboolist0)
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
val myboolist1 =
|
|
Yoneda_psi(functor_list0){bool}(Yoneda_bool_list0)
|
|
//
|
|
(* ****** ****** *)
|
|
|
|
val () = fprintln! (stdout_ref, "myboolist0 = ", myboolist0)
|
|
val () = fprintln! (stdout_ref, "myboolist1 = ", myboolist1)
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement main0 () = ()
|
|
|
|
(* ****** ****** *)
|
|
|
|
(* end of [YonedaLemma.dats] *)
|