module Haskell.Prim.Tuple where

open import Haskell.Prim

variable
  as : List Set

--------------------------------------------------
-- Tuples

infixr 5 _;_
record Pair (A B : Set) : Set where
  constructor _;_
  field fst : A ; snd : B

Tuple : List Set  Set
Tuple [] = 
Tuple (A  AS) = Pair A (Tuple AS)

infix 3 _×_ _×_×_

_×_ : (a b : Set)  Set
a × b = Tuple (a  b  [])

_×_×_ : (a b c : Set)  Set
a × b × c = Tuple (a  b  c  [])

infix -1 _,_ _,_,_

pattern _,_     x y     = x ; y ; tt
pattern _,_,_   x y z   = x ; y ; z ; tt

uncurry : (a  b  c)  a × b  c
uncurry f (x , y) = f x y

curry : (a × b  c)  a  b  c
curry f x y = f (x , y)

fst : a × b  a
fst (x , _) = x

snd : a × b  b
snd (_ , y) = y

first : (a  b)  a × c  b × c
first f (x , y) = f x , y

second : (a  b)  c × a  c × b
second f (x , y) = x , f y

_***_ : (a  b)  (c  d)  a × c  b × d
(f *** g) (x , y) = f x , g y