1	# Element- and length-indexed sequence model. Random get is O(index);
2	# runtime dense storage is Array<Element>, not this sequential observation.
3	import Base
4	
5	law Values:
6	  for -Element: Data
7	  for length: Nat
8	  Data
9	
10	type Elements<-Element: Data,-length: Nat> is Data:
11	  Elements{head: Element,tail: Values(Element,length)}
12	
13	def Values(Element,length):
14	  match length:
15	    case 0n: Unit
16	    case 1n+rest: Elements<Element,rest>
17	
18	law Index:
19	  for length: Nat
20	  Data
21	
22	type Position<-length: Nat> is Data:
23	  First{}
24	  Next{index: Index(length)}
25	
26	def Index(length):
27	  match length:
28	    case 0n: Empty
29	    case 1n+rest: Position<rest>
30	
31	def index_value(length: Nat,index: Index(length)) -> Nat:
32	  match length:
33	    case 0n:
34	      match index:
35	    case 1n+rest:
36	      match index:
37	        case First{}: 0n
38	        case Next{index}: 1n+index_value(rest,index)
39	
40	def tabulate(~Element: Data,~Context: Data,~sample: Context -> Nat -> Element,length: Nat,+offset: Nat,+context: Context) -> Values(Element,length):
41	  match length:
42	    case 0n: Unit{}
43	    case 1n+rest:
44	      Elements{sample(context,offset),tabulate(~Element,~Context,~sample,rest,1n+offset,context)}
45	
46	def get(-Element: Data,length: Nat,index: Index(length),vector: Values(Element,length)) -> Element:
47	  match length:
48	    case 0n:
49	      match index:
50	    case 1n+rest:
51	      match index:
52	        case First{}:
53	          Elements{head,tail} = vector
54	          head
55	        case Next{index}:
56	          Elements{head,tail} = vector
57	          get(Element,rest,index,tail)
58	
59	def replicate(-Element: Data,length: Nat,+value: Element) -> Values(Element,length):
60	  match length:
61	    case 0n: Unit{}
62	    case 1n+rest: Elements{value,replicate(Element,rest,value)}
63	
64	
65	def zip_map(~Element: Data,~Context: Data,~combine: Context -> Element -> Element -> Element,
66	  length: Nat,+context: Context,left: Values(Element,length),right: Values(Element,length)) -> Values(Element,length):
67	  match length:
68	    case 0n: Unit{}
69	    case 1n+rest:
70	      Elements{left_head,left_tail} = left
71	      Elements{right_head,right_tail} = right
72	      Elements{combine(context,left_head,right_head),zip_map(~Element,~Context,~combine,rest,context,left_tail,right_tail)}