Formal Representation of Haskell Data-Types I come from Haskell programming and currently writing my (Diploma/Master) thesis. I'm having trouble finding a formal/mathematical notation for a Haskell data-type.

The Haskell data type is:

data ARE = ARE [(ARF, ARF)] [ARF]   -- Haskell form
type ARE = ( [(ARF, ARF)], [ARF] )  -- alternate form


An ARE is an affine randomized encoding and an ARF is an affine randomized function. You can think of an ARF just as an abstract entity, just like a field or group element. My problem is how to formally notate a definition for an ARE.

First, I'll try to describe what an ARE is in english: An ARE is a tuple (in the "alternate form", in my Haskell program it's represented as in the "Haskell form") containing:


a list (not a set since it could contain duplicates) containing tuples. Each of these tuples is just two ARFs
a list of ARFs


What I'm looking for is a formal notation of such an ARE.

(edit: removed nonsense notation proposal...)

About the expected audience (and their knowledge domain) of my thesis: I will provide Haskell code, but the entire thesis should be understandable by someone who is not a programmer (and in particular no Haskell programmer). The reader will need some knowledge in cryptography, computer science (but not programming) and basic mathematics (some field theory, especially the finite fields $\mathbb{F}_{2^n}$). In the text I simply want to tell the reader what AREs are and how I transform general expressions to AREs.
Unter the assumption, that lists simply represents arbitrary sets, the mathematical notation should probably read:


  An ARE is an element of the following set:
  
  $\{ (P, Q) \mid P \subseteq ARF \times ARF, Q \subseteq ARF \} $    


But as you stated, lists in your domain are always finite, ordering is not important, but multiplicity is. Thus, I would model the lists as finite multisets. Using an explicit notation for mulitsets, a possible definition would be:


  An ARE is an element of the following set:
  
  $\{ (P_\chi, Q_\xi) \mid P \subseteq ARF \times ARF, 
                           P~\text{finite},~
                           \chi \in (P \to \mathbb{N}^+),
                           Q \subseteq ARF, Q~\text{finite},~
                           \xi \in (Q \to \mathbb{N}^+) \} $    


Here, the notation $P_\chi$ denotes a multiset with P being the underlying ordinary set and $\chi \in P \to \mathbb{N}^+$ being the multiplicity function of the multiset.