# 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.

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.

• To answer your questions: The order is not important (--> multiset) and the "lists" are finite – Johannes Weiss Aug 16 '12 at 22:38
• My "mathematical" notation was indeed complete nonsense. Besides formatting issues (non-visible curly brackets because I sometimes typed { ... } instead of \{ ... \}), I completely messed it up anyway :-(. Your suggestion using P and Q being subsets of all possible ARFs and $ARF \times ARF$s seems very good. Thanks! – Johannes Weiss Aug 16 '12 at 23:49
• Sorry, unfortunately, I identified one problem: How could one notate that $P$ and $Q$ are multisets? $Q \subseteq ARF$ looks like $Q$ being an ordinary set. – Johannes Weiss Aug 17 '12 at 15:29
• If you look at, for example, multisets on Wikipedia, for better or worse they use the same notation as regular sets. If you're only talking about multisets, I think it's fair to just say "by 'set' I mean 'multiset'" and go from there. – Rob Simmons Aug 18 '12 at 15:51
• @Johannes Weiß: Why don’t you just write “P and Q are multisets” explicitly? I do not think that there is a widely accepted notation for multisets. – Tsuyoshi Ito Aug 18 '12 at 22:25