Collecting isos on regular types

July 15th, 2005 by Thorsten

After Conor’s report from the Scottish Programming Language Workshop, I was talking about my new hobby of collecting isomorphisms on regular types (0,1,+,x,List) and claimed that

\mathrm{List}(A+1)\simeq \mathrm{List}(\mathrm{List} A))

would be such a beast. Conor discovered that this was wrong and the corrected iso is

\mathrm{List}(A+1)\simeq \mathrm{List}(\mathrm{List} A))\times \mathrm{List}(A)

which is indeed an instance of the other beast in my rather modest collection :

\mathrm{List}(A+B) \simeq \mathrm{List}(\mathrm{List}(A)\times B)\times\mathrm{List}(A).

Graham asked about the connection to numbers and Conor was happy to oblige by noting that arithmetically

\mathrm{List}(A) = {1\over{1-a}}

and checking that the general iso is justified by this interpretation.
Since I got bored this afternoon, waiting for a phone call, I hacked in the first iso into Haskell (can I use lhs here? [you can now - Ed])


%format phi = “\phi”
%format phii = “\phi^\prime”
\begin{code}
phi  :: [Maybe a] -> ([[a]],[a])
phi  []        = ([],[])
phi  (an:ans)  =
    case  an of
	     Nothing  -> (as:aas,[])
	     Just a   -> (aas,a:as)
    where (aas,as) = phi ans
\end{code}
\begin{code}
phii  :: ([[a]],[a]) -> [Maybe a]
phii  ([],[])      = []
phii  (as:aas,[])  = Nothing:(phii (aas,as))
phii  (aas,a:as)   = (Just a):(phii (aas,as))
\end{code}

Leave a Reply