What pairings in Idris can look like at least.

Pairing.idr

module Pairing

||| Model different group types.
data GTy = G1 | G2 | GT

||| Group element, implementation is incomplete but shows how dependent types can be used to provide more infomation.
data Element : GTy -> Type where
  MkElement : value -> (ty : GT) -> Element ty

||| Pairing information, implementation is incomplete.
data Pairing 

||| Perform `c = e(a,b), a\in G1, b\inG2, c\in GT`
|||
||| @pairing `e` is the pairing to apply
||| @a       is the first element from G1
||| @b       is the second element from G2
|||
||| Returns the result, an element of GT.
apply : (pairing : Pairing)
     -> (a       : Element G1)
     -> (b       : Element G2)
     -> Element GT