0 | module Data.Fun
 1 |
 2 | import public Data.Vect
 3 |
 4 | %default total
 5 |
 6 | ||| Build an n-ary function type from a Vect of Types and a result type
 7 | public export
 8 | Fun : Vect n Type -> Type -> Type
 9 | Fun [] r = r
10 | Fun (t::ts) r = t -> Fun ts r
11 |
12 | public export
13 | chain : {ts : Vect n Type} -> Fun [r] r' -> Fun ts r -> Fun ts r'
14 | chain {ts = []} g r  = g r
15 | chain {ts = (_::_)} g f = \ x => chain g (f x)
16 |
17 | public export
18 | [Nary] {ts : Vect n Type} -> Functor (Fun ts) where
19 |   map = chain
20 |
21 | ||| Returns the co-domain of a n-ary function.
22 | public export
23 | target : {ts : Vect n Type} -> {r: Type} -> Fun ts r -> Type
24 | target _ = r
25 |