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

use crate::{
  nat_trans::*,
  type_app::*,
};

// Row: RowCon :: (Type -> Type) -> Type
pub trait RowCon
{
}

pub trait RowApp<'a, F : 'a + ?Sized>: RowCon
where
  F : TypeCon,
{
  type Applied: 'a;
}

pub trait RowAppGeneric: RowCon + Sized
{
  fn with_row_app<'a, F : 'a, R : 'a>(
    cont : impl RowAppGenericCont<'a, Self, F, R>
  ) -> R
  where
    Self : 'a,
    F : TypeAppGeneric;
}

pub trait RowAppGenericCont<'a, Row : 'a, F : 'a, R : 'a>
{
  fn on_row_app(self) -> R
  where
    F : TypeCon,
    Row : RowApp<'a, F>;
}

pub trait HasRowApp<'a, Row : 'a + ?Sized, F : 'a + ?Sized + TypeCon>
{
  fn get_applied(self: Box<Self>) -> Box<Row::Applied>
  where
    Row : RowApp<'a, F>;

  fn get_applied_borrow<'b>(&'b self) -> &'b Row::Applied
  where
    Row : RowApp<'a, F>;

  fn get_applied_borrow_mut<'b>(&'b mut self) -> &'b mut Row::Applied
  where
    Row : RowApp<'a, F>;
}

pub type AppRow<'a, Row, F> = Box<dyn HasRowApp<'a, Row, F> + 'a>;

pub fn wrap_row<'a, Row : 'a, F : 'a>(row : Row::Applied) -> AppRow<'a, Row, F>
where
  F : TypeCon,
  Row : RowApp<'a, F>,
{
  Box::new(row)
}

impl<'a, Row : 'a, F : 'a, RF : 'a> HasRowApp<'a, Row, F> for RF
where
  F : TypeCon,
  Row : RowApp<'a, F, Applied = RF>,
{
  fn get_applied(self: Box<Self>) -> Box<RF>
  {
    self
  }

  fn get_applied_borrow(&self) -> &RF
  {
    self
  }

  fn get_applied_borrow_mut(&mut self) -> &mut RF
  {
    self
  }
}

pub trait LiftRow: RowCon
{
  fn lift<'a, F : 'a, G : 'a>(
    trans : impl NaturalTransformation<F, G> + Clone,
    row : AppRow<'a, Self, F>,
  ) -> AppRow<'a, Self, G>
  where
    Self : 'a,
    F : TypeAppGeneric,
    G : TypeAppGeneric;
}