1type Foo a = a -> a 2 3type Bar a = a! -> () 4 5type FooBar a = # 6 { curr : a 7 , foo : Foo a 8 , bar : Bar a 9 } 10 11foobar : all (a) . (a, Foo a, Bar a) -> FooBar a 12foobar (curr, foo, bar) = #{ curr, foo, bar } 13 14funca : all (a,b). (a,b) -> FooBar (a,b) 15funca curr = 16 let foo : Foo (a, b) 17 = \(a, b) => (a, b) 18 and bar : Bar (a,b) 19 = \(a, b) => () 20 in foobar (curr, foo, bar) 21 22funcb : all (a,b). #{ x: a, y: b } -> FooBar #{ x: a, y: b } 23funcb curr = 24 let foo : Foo #{ x: a, y: b } 25 = \(z {x, y}) => #{x, y} 26 and bar : Bar #{ x: a, y: b } 27 = \(z {x, y}) => () 28 in foobar (curr, foo, bar)