module Haskell.Prim.Tuple where

open import Haskell.Prim

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

infix 3 _×_ _×_×_

infix -1 _,_ _,_,_

record _×_ (a b : Set) : Set where
  constructor _,_
  field
    fst : a
    snd : b
open _×_ public

data _×_×_ (a b c : Set) : Set where
  _,_,_ : a → b → c → a × b × c

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)

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

fst₃ : (a × b × c) → a
fst₃ (x , _ , _) = x 

snd₃ : (a × b × c) → b
snd₃ (_ , y , _) = y

thd₃ : (a × b × c) → c
thd₃ (_ , _ , z) = z