tag:blogger.com,1999:blog-6839602Sat, 07 May 2016 14:10:27 +0000GADTsconstructive logicordinalsHaskellLeibniz equalitySimulating Dependent Types with Guarded Algebraic DatatypescountabilityC++CoqGHCHeyting algebraV=L_|_dependent typeseffect inferenceeffectslightweight static capabilitiesnested typesquotient typesreferential transparencyzero-knowledge proofCPOsDependent MLFomegaLiskov substitutabilityMLOOPbugscardinal numbersconferencescontinuitycopious free timedefinabilityflow camlfuzzy logicgrammar checkingimpredicativityinformation flowkindslaypeoplemorphismsparallel orpolymorphismrefinement typessized listsstatic analysisterminationtype disequalityEveryone Else is CrazyA blog about typed programminghttp://blog.jbapple.com/noreply@blogger.com (Jim Apple)Blogger39125tag:blogger.com,1999:blog-6839602.post-4085994718741326245Sat, 22 Mar 2008 21:31:00 +00002008-03-22T14:31:44.534-07:00effect inferenceRegion, Effect and Closure Inference, implemented<a href="http://blog.jbapple.com/2007/06/region-effect-and-closure-inference.html">Last post</a>
<p>
<a href="http://cs.anu.edu.au/people/Ben.Lippmeier/">Ben Lippmeier</a> has posted <a href="http://www.haskell.org/haskellwiki/DDC">an implementation of his region, effect, and closure inference in a Haskell dialect called The Disciplined Disciple Compiler</a>.http://blog.jbapple.com/2008/03/region-effect-and-closure-inference.htmlnoreply@blogger.com (Jim Apple)0tag:blogger.com,1999:blog-6839602.post-6429016332916682162Mon, 17 Mar 2008 04:31:00 +00002011-12-15T22:03:26.251-08:00Types at reddit<a href="http://reddit.com/r/types/">I have created a subreddit for types.</a> (Static analysis is also welcome.)http://blog.jbapple.com/2008/03/types-at-reddit.htmlnoreply@blogger.com (Jim Apple)1tag:blogger.com,1999:blog-6839602.post-728777982527328109Sat, 23 Feb 2008 05:56:00 +00002008-04-08T19:33:27.489-07:00GADTsnested typesTypes, named (was: "Name that type!"), plus two more questionsHere are the answers to <a href="http://blog.jbapple.com/2008/02/name-that-type-nested-types-edition.html">the previous quiz</a>.
<p>
The first datatype holds any factorial number of values. Here it is again, with one small change and a few de-obfuscations:
<pre>
> data FacHelp (f :: * -> *) (y :: *) =
> Stop y
> | More (FacHelp (OneMore f) (f y))
> newtype OneMore (f :: * -> *) (y :: *) =
> OneMore (y, f y)
> newtype Identity y = Identity y
> type Factorial y = FacHelp Identity y
</pre>
<s>
The second is lists of length more than two containing lists of length more than two. This means that no inhabitant contains a prime number of elements. As far as I know, it is unknown whether there is a datatype with every inhabitant containing a prime number of elements. (GADTs can do it, of course, but I'm ignoring those for now, since <a href="http://www.cs.virginia.edu/~jba5b/singleton/Lambda.hs">they can do anything.</a>
(<a href="http://www.haskell.org/pipermail/haskell-cafe/2007-January/021178.html">mirror</a>,
<a href="http://thread.gmane.org/gmane.comp.lang.haskell.cafe/18210/focus=18210">mirror 2</a>,
<a href="http://www.mail-archive.com/haskell-cafe@haskell.org/msg19411.html">mirror 3</a>,
<a href="http://groups.google.com/group/fa.haskell/browse_thread/thread/7741b39b68de7081/16ec8969295ac46c#16ec8969295ac46c">mirror 4</a>)
<p>
Here's that datatype again, renamed:
<pre>
> data LongList x = Two x x
> | AndAnother x (LongList x)
> data Composite x = Composite (LongList (LongList x))
</pre>
</s>
<strong>Update:</strong>
<br>
<a href="http://www.cs.rutgers.edu/~ccshan/">Chung-chieh Shan</a> pointed out to me that I got that datatype wrong. (The other text above is correct, I think.) Anyway, here's his counterexample:
<pre>
> test :: Composite Char
> test = Composite (Two (Two 'a' 'b')
> (AndAnother 'c' (Two 'd' 'e')))
</pre>
This is a correct (I think!) implementation of a container that can't be of a prime size:
<pre>
> data Product f g a = Times (f (g a))
> | LeftIncr (Product (OneMore f) g a)
> | RightIncr (Product f (OneMore g) a)
> newtype Pair a = Pair (a,a)
> type Comp = Product Pair Pair
</pre>
<strong>End update</strong>
<p>
The third datatype uses the type <code>H</code>, which encodes containers with a square number of elements. <code>H</code> is based on the idea that the sequence of partial sums of the sequence of odd natural numbers is the same as the sequence of squares. That is, {0, 1, 1+3, 1+3+5, …} = {0<sup>2</sup>, 1<sup>2</sup>, 2<sup>2</sup>, 3<sup>2</sup>, …}
<p>
We can now use <a href="http://en.wikipedia.org/wiki/Lagrange's_four-square_theorem">Lagrange's four-square theorem</a> to see that question 3(b) is, strangely, a container that can hold any number of elements. An extension of this by Legendre showed <a href="http://mathworld.wolfram.com/LagrangesFour-SquareTheorem.html">[cite]</a> that every number not of the form 4<sup>k</sup>(8m + 7) is representable by the sum of three squares, and this answers question 3(a).
<p>
Here are both parts again, renamed and cleaned up a bit:
<pre>
> data SqHelp x y = End
> | Extra x (SqHelp (y,y,x) y)
> type Square a = SqHelp a a
> data Legendre x = Legendre (Square x) (Square x) (Square x)
> data Lagrange x = Lagrange (Square x) (Legendre x)
</pre>
Here are two more questions:
<br>
4. Can we write something analogous to 3(a) in a more direct way?
<br>
5.
<pre>
> data M a b = N b
> | O (M (a,b) a)
> newtype P a = P (M a a)
</pre>http://blog.jbapple.com/2008/02/types-named-was-name-that-type-plus-two.htmlnoreply@blogger.com (Jim Apple)4tag:blogger.com,1999:blog-6839602.post-7473091652753951323Fri, 22 Feb 2008 11:25:00 +00002008-02-22T09:21:56.362-08:00GADTsLeibniz equalitynested typesName that type! (nested types edition)<!-- <a href="http://www.cs.virginia.edu/~jba5b/singleton/Lambda.hs">Guarded
algebraic datatypes are strong enough to write datatypes that
represent recursively enumerable sets.</a>
(<a href="http://www.haskell.org/pipermail/haskell-cafe/2007-January/021178.html">mirror</a>,
<a href="http://thread.gmane.org/gmane.comp.lang.haskell.cafe/18210/focus=18210">mirror 2</a>,
<a href="http://www.mail-archive.com/haskell-cafe@haskell.org/msg19411.html">mirror 3</a>,
<a href="http://groups.google.se/group/fa.haskell/tree/browse_frm/month/2007-01/b3b8d1c7642923d5?rnum=181&_done=%2Fgroup%2Ffa.haskell%2Fbrowse_frm%2Fmonth%2F2007-01%3F#doc_16ec8969295ac46c">mirror 4</a>)
That is, they are are strong as
you could possibly expect. We can even write
datatypes with such strong encodings without GADTs by using Leibniz equality, though we
can't perform all of the operations on them we might hope to
without <a href="http://ecommons.library.cornell.edu/bitstream/1813/5614/1/TR2003-1901.pdf">first-class
phantom
types</a>. (<a href="http://homepages.inf.ed.ac.uk/jcheney/publications/errata.html#fcpt-tr">errata</a>)
(See also <a href="http://homepage.mac.com/pasalic/p2/">Emir Pasalic</a>'s
<a href="http://homepage.mac.com/pasalic/p2/papers/thesis.pdf">thesis</a>,
Chapter 4: Equality Proofs, p. 72 in your PDF reader, p. 62 in your
printed copy)
<p>
Type equality, whether from Leibniz or GADTs, is not necessary to
write datatypes that enforce useful invariants, however. A simple
example is that of a complete binary tree. A regular binary tree can
be encoded as:
-->
<div style="background-color: #ffb; text-align: center; border: solid 1px; padding: 1em;"><a href="#quiz">Jump to the bottom for the quiz</a></div>
<p>
If we want to write a type for binary trees in Haskell, it is easy to do so:
<pre>
> data BinaryTree a = Leaf
> | InternalNode (BinaryTree a) a (BinaryTree a)
</pre>
The structure of the type guarantees certain things about its
inhabitants. For instance, every node has exactly two children. If we
want to guarantee stronger invariants, we can change the shape of the
type. We can write a a type for <dfn>complete</dfn>
binary tree (that is, binary trees in which every leaf is at the same
depth), as
<pre>
> data CompleteBinaryTree a = Leaves
> | NonLeaves a (CompleteBinaryTree (a,a))
</pre>
The argument in the recursive part of this datatype is not the same as
it is in the declaration. Datatypes with this property are
called <dfn>nested</dfn> or <dfn>non-regular</dfn>
or <dfn>heterogeneous</dfn> or <dfn>non-uniform</dfn>. We can express
all sorts of invariants with these datatypes. Here's another example:
<pre>
> data AList a b = Nil
> | Cons a (AList b a)
</pre>
If we want to manipulate lists that alternate between two
types <code>a</code> and <code>b</code>, we could use the
type <code>[Either a b]</code>, but this doesn't ensure that we don't
have two <code>a</code>s or two <code>b</code>s in a row. We could,
instead, use the type <code>[(a,b)]</code>, but this would only allow
us to create lists of even length. By switching the position of the
parameters in the recursion in <code>AList</code>, we can represent
alternating lists of any length.
<p>
Here are some other examples of data structure invariants we can ensure with nested types:
<ul>
<li> <a href="http://www.cs.nott.ac.uk/~nhn/TFP2006/Papers/27-GhaniHamanaUustaluVene-CyclicStructuresAsNestedDatatypes.pdf">Cyclic
data structures</a> (<a href="http://cs.ioc.ee/~tarmo/papers/tfp06.pdf">mirror</a>)
<li> Many different types of lists with
fast <code>cons</code>, <code>snoc</code>, concatenation, and indexing,
including
<ul>
<li> <a href="http://www.soi.city.ac.uk/~ross/papers/FingerTree.html">Finger
trees</a>
(<a href="http://www.informatik.uni-bonn.de/~ralf/publications/FingerTrees.pdf">mirror</a>,
<a href="http://web.comlab.ox.ac.uk/oucl/work/ralf.hinze/publications/FingerTrees.pdf">mirror 2</a>)
<li>
<a href="http://www.eecs.usma.edu/webs/people/okasaki/pubs.html#cup98">Binary random-access lists, catenable lists, and
catenable deques</a>
(<a href="http://www.cs.cmu.edu/~rwh/theses/okasaki.pdf">earlier version</a>,
<a href="http://www.cs.cmu.edu/afs/cs/project/fox/mosaic/papers/cokasaki-thesis.ps">earlier version mirror</a>,
<a href="http://citeseer.ist.psu.edu/okasaki98purely.html">earlier version mirror 2</a>,
<a href="http://cybertiggyr.com/gene/amo/amo.html">notes and answers to exercises</a>)
<li>
<a href="http://www.informatik.uni-bonn.de/~ralf/publications/DSDesign.ps.gz">Rightist
right-perfect trees</a> (<a href="http://web.comlab.ox.ac.uk/oucl/work/ralf.hinze/publications/DSDesign.ps.gz">mirror</a>)
<ul>
<li>
<a href="http://www.informatik.uni-bonn.de/~ralf/publications/WAAAPL99a.ps.gz">earlier version</a>,
<a href="http://citeseer.ist.psu.edu/hinze99manufacturing.html">earlier version mirror</a>,
<a href="http://web.comlab.ox.ac.uk/oucl/work/ralf.hinze/publications/WAAAPL99a.ps.gz">earlier version mirror 2</a>
<li>
<a href="http://www.informatik.uni-bonn.de/~ralf/publications/IAI-TR-99-5.ps.gz">even earlier version</a>,
<a href="http://www.informatik.uni-bonn.de/III/forschung/publikationen/tr/reports/IAI-TR-99-5.ps.gz">even earlier version mirror</a>,
<a href="http://web.comlab.ox.ac.uk/oucl/work/ralf.hinze/publications/IAI-TR-99-5.ps.gz">even earlier version mirror 2</a>
</ul>
</ul>
<li> <a href="http://reddit.com/info/w1oz/comments/cwbrz">Red-black trees</a> (<a href="http://www.cs.kent.ac.uk/pubs/2001/1293/index.html">a paper</a>,
<a href="http://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html">code for that paper</a>),
<a href="http://www.haskell.org/pipermail/haskell/2003-April/011693.html">AVL trees</a>
(<a href="http://osdir.com/ml/lang.haskell.general/2003-04/msg00120.html">mirror</a>,
<a href="http://www.cse.unsw.edu.au/~dons/haskell-1990-2006/msg14064.html">mirror 2</a>)
<li> <a href="http://www.eecs.usma.edu/webs/people/okasaki/icfp99.ps">Square matrices</a>,
triangular matrices
(<a href="http://www.irit.fr/~Ralph.Matthes/works.html">in various works by Ralph Matthes</a>), Toeplitz matrices,
rectangular matrices (see "Manufacturing Datatypes", above)
<li> Efficient-merge heaps (see Okasaki's thesis & book, above), Braun
trees, left-complete trees (see "Manufacturing Datatypes", above)
<li> <a href="http://web.comlab.ox.ac.uk/oucl/work/ralf.hinze/publications/IAI-TR-98-12.ps.gz">Binomial queues</a>
(<a href="http://www.informatik.uni-bonn.de/~ralf/publications/IAI-TR-98-12.ps.gz">mirror</a>,
<a href="http://citeseer.ist.psu.edu/hinze98numerical.html">mirror 2</a>)
<li> <a href="http://www.informatik.uni-bonn.de/~ralf/publications/GGTries.ps.gz">Tries</a>
(<a href="http://web.comlab.ox.ac.uk/oucl/work/ralf.hinze/publications/GGTries.ps.gz">mirror</a>,
<a href="http://citeseer.ist.psu.edu/233124.html">mirror 2</a>,
<a href="http://www.informatik.uni-bonn.de/~ralf/publications/GGTries/index.html">code</a>,
<a href="http://web.comlab.ox.ac.uk/oucl/work/ralf.hinze/publications/GGTries/index.html">code mirror</a>,
<a href="http://www.informatik.uni-bonn.de/~ralf/publications/IAI-TR-98-11.ps.gz">old version</a>,
<a href="http://web.comlab.ox.ac.uk/oucl/work/ralf.hinze/publications/IAI-TR-98-11.ps.gz">old version mirror</a>)
(See also Okasaki's thesis & book)
<li> <a href="http://citeseer.ist.psu.edu/bird98de.html">Well-formed terms in the locally-nameless lambda calculus</a>
(<a href="http://web.comlab.ox.ac.uk/oucl/work/richard.bird/online/BirdPaterson99DeBruijn.pdf">mirror</a>)
</ul>
<a name="quiz">
Finally, here are 3.5 examples of nested types I haven't seen
elsewhere. See if you can figure out what they do.
<pre>
> data A x y = B (x y)
> | C (A (D x) (x y))
> newtype D x y = D (y,x y)
> newtype K x = K x
> type QuestionOne = A K
>
> data E x = F x x
> | G x (E x)
> data QuestionTwo x = Q2 (E (E x))
>
> data H x y = I
> | J y x x (H (y,x) y)
> type L = H ()
> data QuestionThreePartA x = Q3a (L x) (L x) (L x)
> data QuestionThreePartB x = Q3b (L x) (QuestionThreePartA x)
</pre>
</a>http://blog.jbapple.com/2008/02/name-that-type-nested-types-edition.htmlnoreply@blogger.com (Jim Apple)7tag:blogger.com,1999:blog-6839602.post-8751252559920937913Sun, 17 Feb 2008 23:02:00 +00002008-02-17T15:59:29.569-08:00Leibniz equalityLiskov substitutabilityLeibniz and LiskovLeibniz equality of two types <code>a</code> and <code>b</code> is the proposition that in any context, one can be substituted for the other:
<pre>
f a -> f b
</pre>
A value of this type brings to the value level the proof that two types are equal. The only value of this type is the identity function.
<p>
<a href="http://en.wikipedia.org/wiki/Liskov_substitution_principle">The Liskov substitution principle</a> is very similar to Leibniz equality, but only in the contravariant position: If a function takes an argument of type <code>b</code> and <code>a</code> is a subtype of <code>b</code>, then the function must accept an argument of type <code>a</code>. If <code>f</code> is a type constructor that uses its argument only negatively, then <code>a</code> is a subtype of <code>b</code> if there is a value of type
<pre>
f b -> f a
</pre>
For example, <code>λx . x -> b</code> uses <code>x</code> negatively, and any <code>b -> b</code> is also trivially an <code>a -> b</code> when <code>a</code> is a subtype of <code>b</code>. The only value of type <code>f b -> f a</code> is the <code>cast</code> function.
<p>
Let's write the kind for type constructors that use their argument negatively as <code>* -(-)-> *</code> rather than just <code>* -> *</code>, and the kind for type constructors that use their argument positively as <code>* -(+)-> *</code>. Then, the following terms should validate our understanding that supertyping is dual to subtyping:
<pre>
dual : ∀ a:* . ∀ b:* . ∀ g: * -(+)-> * . (∀ f: * -(-)-> * . f b -> f a) -> g a -> g b
dual |a |b |g less bot = less [λx:* . g x -> g b] (λy:g b . y:g b) bot
dual' : ∀ a:* . ∀ b:* . ∀ f: * -(-)-> * . (∀ g: * -(+)-> * . g a -> g b) -> f b -> f a
dual' |a |b |f more top = more [λx:* . f x -> f a] (λy:f a . y:f a) top
</pre>
So subtyping, like type equality, can be brought to the value domain. I now have two questions:
<ol>
<li>Is there an analogue of <a href="http://research.microsoft.com/~simonpj/papers/ext-f/">F<sub>C</sub></a> (<a href="http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html">mirror</a>) for <a href="http://gatekeeper.dec.com/pub/DEC/SRC/research-reports/abstracts/src-rr-080.html">F<sub><:</sub></a>
(<a href="http://lucacardelli.name/Papers/FSub.pdf">mirror 1</a>,
<a href="http://research.microsoft.com/Users/luca/Papers/FSub.A4.pdf">mirror 2</a>,
<a href="http://citeseer.ist.psu.edu/cardelli91extension.html">mirror 3</a>)?
<li>Is there a problem similar to <a href="http://blog.jbapple.com/2007/08/leibniz-equality-decomposition-and.html">decomposition</a> for Liskov substitutability?
</ol>http://blog.jbapple.com/2007/11/leibniz-and-liskov.htmlnoreply@blogger.com (Jim Apple)0tag:blogger.com,1999:blog-6839602.post-8391585046753089908Thu, 10 Jan 2008 07:02:00 +00002008-03-23T16:55:05.270-07:00GADTslightweight static capabilitiespolymorphismrefinement typesExtra type safety using polymorphic types as first-level refinements<p>
This post is literate Haskell.
<p>
I will demonstrate a new technique for using polytypes as first-level <a href="http://www.cs.ucla.edu/~palsberg/tba/papers/freeman-thesis94.pdf">refinement types</a>. (<a href="http://citeseer.ist.psu.edu/225858.html">mirror</a>). The goal, as usual, is for types to better express program invariants and ensure programs are safe.
<p>
I'm going to demonstrate using the <code>risers</code> function, as presented in <a href="http://www.cl.cam.ac.uk/~nx200">Dana N. Xu</a>'s <a href="http://research.microsoft.com/Users/simonpj/papers/verify/escH-hw.ps">ESC/Haskell</a> (<a href="http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps">mirror</a>), which references <a href="http://www-users.cs.york.ac.uk/~ndm">Neil Mitchell</a>'s <a href="http://www-users.cs.york.ac.uk/~ndm/catch/">Catch</a>.
<pre>
> {-# OPTIONS -fglasgow-exts #-}
> -- The LANGUAGE pragma is usually a pain for exploratory programming.
</pre>
<p>
Below are the <code>risers</code> functions as presented by Xu and
Mitchell. They are the same function, though slightly syntacticly
different. <code>risers</code> returns the sorted sublists of a
list.
<p>
Risers has two properties that we are going to discuss:
<ol>
<li> None of the lists in the returned value are empty
<li> If the argument is non-empty, the return value is also non-empty.
</ol>
<pre>
> risersXu :: (Ord t) => [t] -> [[t]]
> risersXu [] = []
> risersXu [x] = [[x]]
> risersXu (x:y:etc) =
> let ss = risersXu (y : etc)
> in case x <= y of
> True -> (x : (head ss)) : (tail ss)
> False -> ([x]) : ss
>
> risersMitchell :: Ord a => [a] -> [[a]]
> risersMitchell [] = []
> risersMitchell [x] = [[x]]
> risersMitchell (x:y:etc) = if x <= y
> then (x:s):ss
> else [x]:(s:ss)
> where (s:ss) = risersMitchell (y:etc)
</pre>
<p>
Neither one of these functions is obviously safe. Xu uses head and
tail and ESC/Haskell to create a proof of their safety. The unsafe part
of Mitchell's code is the <code>where</code> clause, and Mitchell also presents a
tool to prove this safe.
<p>
Our goal will be to write this function in a safe way, with a type
signature that ensures the two properties we expect from the function.
We also aim to do this without having to change the shape of the code,
only the list implementation we are using.
<p>
The present unsafe operations in risersXu and risersMitchell depend on
the second property of the function: non-null inputs generate non-null
outputs. We could write a type for this functions using <a href="http://okmij.org/ftp/Computation/lightweight-dependent-typing.html">a trusted
library with phantom types for branding</a> (<a href="http://www.cs.rutgers.edu/~ccshan/capability/lightweight-static-capabilities.pdf">paper mirror</a>). This technique (called lightweight static capabilities) can do this
and much else as well, but since clients lose all ability to pattern match
(even in case), risers becomes much more verbose. We could also write
a type signature guaranteeing this by using GADTs. Without using one
of these, incomplete pattern matching or calling unsafe <code>head</code> and <code>tail</code>
on the result of the recursive call seems inevitable.
<p>
Here's another way to write the function which does away with the need
for the second property on the recursive call, substituting instead the
need for the first property that no lists in the return value are
empty:
<pre>
> risersAlt :: (Ord t) => [t] -> [[t]]
> risersAlt [] = []
> risersAlt (x:xs) =
> case risersAlt xs of
> [] -> [[x]]
> w@((y:ys):z) ->
> if x <= y
> then (x:y:ys):z
> else ([x]):w
> ([]:_) -> error "risersAlt"
</pre>
<p>
The error is never reached.
<p>
Though ensuring the second property with our usual types seems tricky, ensuring the first is not too tough:
<pre>
> type And1 a = (a,[a])
>
> risersAlt' :: Ord a => [a] -> [And1 a]
> risersAlt' [] = []
> risersAlt' (x:xs) =
> case risersAlt' xs of
> [] -> [(x,[])]
> w@(yys:z) ->
> if x <= fst yys
> then (x,fst yys : snd yys):z
> else (x,[]):w
</pre>
<p>
It is now much easier to see that risers is safe: There is one pattern
match and one case, and each is simple. No unsafe functions like head
or tail are called. It does have three disadvantages, however.
<p>
First, the second property is still true, but the function type does
not enforce it. This means that any other callers of risers may have
to use incomplete pattern matching or unsafe functions, since they may
not be so easy to transform. It is my intuition that it is not
frequently the case that these functions are tricky to transform, but
<a href="http://neilmitchell.blogspot.com/search/label/catch">perhaps
Neil Mitchell disagrees</a>.
<p>
We could fix this by writing another risers function with
type <code>And1 a -> And1 (And1 a)</code>, but this brings us to
the second problem: <code>And1 a</code> is not a subtype
of <code>[a]</code>. This means that callers of our hypothetical other
<code>risers</code> function (as well as consumers of the output
from <code>risersAlt'</code>) must explicitly coerce the results back
to lists.
<p>
Finally, if we are wrong about the first property, and risers does
return an empty list for some non-empty input <code>i</code>, then for any <code>x</code>,
<code>risers (x:i)</code> is <code>_|_</code>, while <code>risersAlt'
(x:i)</code> is <code>[(x,[])]</code>. Thus, the equivalence of these
two function definitions depends on the truth of the second property
on the first function, which is something we were trying to get out of
proving in the first place! Of course, if we're interested in the correctness of
<code>risersAlt'</code>, rather than its equivalence with <code>risersXu</code> or
<code>risersMitchell</code>, then it is not to difficult to reason
about. But part of the point of this was to get they compiler to do some
of this reasoning for us, without having to change the shape of the
code.
<p>
Let's write more expressive signatures using something we may have noticed when using GHCi. The only value of type <code>forall a. [a]</code> (excluding lists of _|_s) is <code>[]</code>. Every value of type <code>forall a . Maybe a</code> is <code>Nothing</code>, and every <code>forall a . Either a Int</code> has an <code>Int</code> in <code>Right</code>. Andrew Koenig <a href="http://www.usenix.org/publications/library/proceedings/vhll/koenig.html">noticed something similar when learning ML</a> (<a href="http://web.archive.org/web/20070222202543/http://www.usenix.org/publications/library/proceedings/vhll/full_papers/koenig.a">archived</a>), and the <a href="http://www.haskell.org/ghc/docs/latest/html/libraries/base/Control-Monad-ST.html">ST monad</a> operates on a similar principle. (<a href="http://citeseer.ist.psu.edu/launchbury96state.html">paper with details about ST</a>, <a href="http://www.cse.ogi.edu/~jl/Papers/stateThreads.ps">mirror</a>)
<pre>
> data List a n = Nil n
> | forall r . a :| (List a r)
</pre>
<p>
The only values of type <code>forall a . List a n</code> use the <code>Nil</code> constructor, and the only values of type <code>forall n . List a n</code> use the <code>:|</code> constructor.
<pre>
> infixr :|
>
> box x = x :| Nil ()
>
> type NonEmpty a = forall n . List a n
>
> onebox :: NonEmpty Int
> onebox = box 1
>
> onebox' :: List Int Dummy
> onebox' = onebox
>
> data Dummy
>
> -- This doesn't compile
> -- empty :: NonEmpty a
> -- empty = Nil ()
</pre>
<p>
<code>NonEmpty a</code> is a subtype of <code>List a x<code> for all types <code>x</code>.
<pre>
> data Some fa = forall n . Some (fa n)
>
> safeHead :: NonEmpty a -> a
> safeHead x = unsafeHead x where
> unsafeHead (x :| _) = x
>
> safeTail :: NonEmpty a -> Some (List a)
> safeTail x = unsafeTail x where
> unsafeTail (_ :| xs) = Some xs
</pre>
<p>
Unfortunately, we'll be forced to <code>Some</code> and un-<code>Some</code> some values, since Haskell does not have first-class existentials, and it takes some thinking to see that <code>safeHead</code> and <code>safeTail</code> are actually safe.
<p>
Here is a transformed version of Mitchell's risers:
<pre>
> risersMitchell' :: Ord a => List a n -> List (NonEmpty a) n
> risersMitchell' (Nil x) = (Nil x)
> risersMitchell' (x :| Nil _) = box (box x)
> risersMitchell' ((x {- :: a -}) :| y :| etc) =
> case risersMitchell' (y :| etc) {- :: NonEmpty (NonEmpty a) -} of
> Nil _ -> error "risersMitchell'"
> s :| ss -> if x <= y
> then (x :| s) :| ss
> else (box x) :| s :| ss
</pre>
<p>
Since we can't put the recursive call in a where clause, we must use a case with some dead code. The type annotations are commented out here to show they are not needed, but uncommenting them shows that the recursive call really does return a non-empty lists, and so the <code>Nil</code> case really is dead code.
<p>
This type signature ensures both of the properties listed when introducing <code>risers</code>. The key to the non-empty-arguments-produce-non-empty-results property is that the variable <code>n</code> in the signature is used twice. That means applying <code>risersMitchell'</code> to a list with a fixed (or existential) type as its second parameter can't produce a <code>NonEmpty</code> list.
<pre>
> risersXu' :: Ord a => List a r -> List (NonEmpty a) r
> risersXu' (Nil x) = Nil x
> risersXu' (x :| Nil _) = box (box x)
> risersXu' (((x :: a) :| y :| etc) :: List a r) =
> let ss = risersXu' (y :| etc)
> in case x <= y of
> True -> case safeTail ss of
> Some v -> (x :| (safeHead ss)) :| v
> False -> (box x) :| ss
</pre>
<p>
Here we see that the type annotation isn't necessary to infer that <code>risers</code> applied to a non-empty list returns a non-empty list. The value <code>ss</code> isn't given a type signature, but we can apply <code>safeHead</code> and <code>safeTail</code>. The case matching on <code>safeTail</code> is the pain of boxing up existentials.
<p>
This is the first version of <code>risers</code> with a type signature that gives us the original invariant Xu and Mitchell can infer, as well as calling no unsafe functions and containing no incomplete case or let matching. It also returns a list of lists, just like the original function, and has a definition in the same shape.
<p>
With first-class existentials, this would look just like Xu's <code>risers</code> (modulo built-in syntax for lists). With let binding for polymorphic values, <code>risersMitchell'</code> would look just like Mitchell's original risers, but be safe by construction. Let binding for polymorphic values would also allow non-trusted implementations of <code>safeTail</code> and
<code>safeHead</code> to be actually safe.
<p>
For contrast, here is a GADT implementation of risers:
<pre>
> data GList a n where
> GNil :: GList a IsNil
> (:||) :: a -> GList a m -> GList a IsCons
>
> infixr :||
>
> data IsNil
> data IsCons
>
> gbox x = x :|| GNil
>
> risersMitchellG :: Ord a => GList a n -> GList (GList a IsCons) n
> risersMitchellG GNil = GNil
> risersMitchellG (c :|| GNil) = gbox $ gbox c
> risersMitchellG (x :|| y :|| etc) =
> case risersMitchellG (y :|| etc) of
> -- GHC complains, "Inaccessible case alternative: Can't match types `IsCons' and `IsNil'
> -- In the pattern: GNil"
> -- GNil -> error "risers"
> s :|| ss ->
> if x <= y
> then (x :|| s) :|| ss
> else (gbox x) :|| s :|| ss
</pre>
<p>
This is safe and has its safety checked by GHC. It also does not require existentials, though when using this encoding, many other list functions (such as filter) will.
<p>
Now here is a lightweight static capabilities version of risers:
<pre>
> -- module Protected where
>
> -- Export type constructor, do not export value constructor
> newtype LWSC b a = LWSC_do_not_export_me [a]
>
> data Full
> type FullList = LWSC Full
>
> data Any
>
> lnil :: LWSC Any a
> lnil = LWSC_do_not_export_me []
>
> lcons :: a -> LWSC b a -> FullList a
> lcons x (LWSC_do_not_export_me xs) = LWSC_do_not_export_me (x:xs)
>
> lwhead :: FullList a -> a
> lwhead (LWSC_do_not_export_me x) = head x
>
> data Some' f n = forall a . Some' (f a n)
>
> lwtail :: FullList a -> Some' LWSC a
> lwtail (LWSC_do_not_export_me a) = Some' (LWSC_do_not_export_me (tail a))
>
> deal :: LWSC b a -> LWSC Any c -> (FullList a -> FullList c) -> LWSC b c
> deal (LWSC_do_not_export_me []) _ _ = LWSC_do_not_export_me []
> deal (LWSC_do_not_export_me x) _ f =
> case f (LWSC_do_not_export_me x) of
> LWSC_do_not_export_me z -> LWSC_do_not_export_me z
>
> nullcase :: LWSC b a -> c -> (FullList a -> c) -> c
> nullcase (LWSC_do_not_export_me []) z _ = z
> nullcase (LWSC_do_not_export_me x) _ f = f (LWSC_do_not_export_me x)
>
> -- module Risers where
>
> lbox x = lcons x lnil
>
> risersXuLW :: Ord a => LWSC b a -> LWSC b (FullList a)
> risersXuLW x =
> deal x
> lnil
> (\z -> let x = lwhead z
> in case lwtail z of
> Some' rest ->
> nullcase rest
> (lbox (lbox x))
> (\yetc ->
> let y = lwhead yetc
> etc = lwtail yetc
> ss = risersXuLW yetc
> in if x <= y
> then case lwtail ss of
> Some' v -> lcons (lcons x $ lwhead ss) v
> else lcons (lbox x) ss))
</pre>
<p>
There is a good bit of code that must go in the protected module, including two different functions for case dispatch. These functions are used instead of pattern matching, and make the definition of risers much more verbose, though I may not have written it with all the <a href="http://arcanux.org/lambdacats/type-woes.jpg">oleg-magic</a> possible to make it more usable.
<p>
Out of the three, I think GADTs are still the winning approach, but it's fun to explore this new idea, especially since Haskell doesn't have traditional subtyping.http://blog.jbapple.com/2008/01/extra-type-safety-using-polymorphic.htmlnoreply@blogger.com (Jim Apple)1tag:blogger.com,1999:blog-6839602.post-3028825677574535690Mon, 07 Jan 2008 01:36:00 +00002008-01-06T17:47:51.397-08:00conferencesPOPL 2008 and affiliated eventsThis week is <a href="http://www.cs.ucsd.edu/popl/08/#AffiliatedEvents">POPL and affiliated events</a>. I'll be at the first and third days of <a href="http://www1.cs.uic.edu/vmcai08/index.php">VMCAI</a>, <a href="http://www.cis.upenn.edu/~plclub/popl08-tutorial/">the Coq tutorial</a>, and POPL itself. Unfortunately, I'll have to miss <a href="http://www.program-transformation.org/PEPM08">PEPM</a>.http://blog.jbapple.com/2008/01/popl-2008-and-affiliated-events.htmlnoreply@blogger.com (Jim Apple)0tag:blogger.com,1999:blog-6839602.post-8473302617671836402Fri, 28 Dec 2007 05:15:00 +00002007-12-27T21:17:09.264-08:00dependent typesHaskellA common language for dependently-typed programming?<a href="http://research.microsoft.com/~simonpj/papers/history-of-haskell/index.htm">The Haskell project was begun in order to unify "more than a dozen non-strict, purely functional programming languages".</a> (<a href="http://portal.acm.org/ft_gateway.cfm?id=1238856&type=pdf">mirror</a>) We are rapidly approaching that many viable choices for programming with dependent types.
<ol>
<li>
<a href="http://www.e-pig.org/">Epigram</a>
<li>
<a href="http://www.ats-lang.org/">ATS</a> (successor to <a href="http://cs-www.bu.edu/~hwxi/DML/DML.html">Dependent ML</a> and <a href="http://www.cs.bu.edu/~hwxi/Xanadu/Xanadu.html">Xanadu</a>)
<li>
<a href="http://unit.aist.go.jp/cvs/Agda/">Agda</a> (successor to <a href="http://www.cs.chalmers.se/%7Eaugustss/cayenne/">Cayenne</a>)
<li>
<a href="http://web.cecs.pdx.edu/~sheard/Omega/index.html">Ωmega</a>
<li>
<a href="http://www.nuprl.org/">NuPrl</a>
<li>
<a href="http://twelf.plparty.org/">Twelf</a>
<li>
<a href="http://isabelle.in.tum.de/">Isabelle</a>
<li>
<a href="http://coq.inria.fr/">Coq</a>
<li>
<a href="http://cs-www.cs.yale.edu/homes/delphin/">Delphin</a>
<li>
<a href="http://www.metaocaml.org/concoqtion/">Concoqtion</a>
<li>
<a href="http://www.aldor.org/">Aldor</a>
<li>
<a href="http://www.guru-lang.org/">Guru</a> (successor to <a href="http://cl.cse.wustl.edu/papers/rsp1-tech.pdf">RSP1</a>)
</ol>
And now, a list of caveats about the above list:
<ul>
<li>
Some of the items on this list are theorem provers first and dependently-typed programming languages second. <a href="http://www.cs.berkeley.edu/~adamc/papers/PositionPLPV06/">Adam Chlipala argues that this is not such a problem for Coq</a>.
<li>
This list does not include several languages that are new or new variants (<a href="http://www.seas.upenn.edu/~sweirich/papers/tfp07.pdf">PIE</a>, <a href="http://matita.cs.unibo.it/">Matita</a>), not checked at compile-time (<a href="http://sage.soe.ucsc.edu/">Sage</a>), or not actively maintained (<a href="http://www.cs.ru.nl/~freek/digimath/bycategory.html#tacticprover">most proof assistants</a>, <a href="http://pll.cpsc.ucalgary.ca/charity1/www/home.html">Charity</a>).
<li>
Some of these choices may not be real options for programing with dependent types. Twelf is designed for programming about programming languages, and, if I remember correctly, doesn't have parametric polymorphism because of something having to do with higher-order abstract syntax. Aldor can't understand most type equalities, making its dependent types somewhat weak, though <a href="http://www.cs.kent.ac.uk/people/staff/sjt/Atypical/">Atypical and Aldor-- aimed to remedy this five years ago</a>. Agda and Epigram have New Exciting Versions 2 coming out, so they suffer from <a href="http://en.wikipedia.org/wiki/Osborne_Effect">the Osborne Effect</a>.
</ul>
Is it time yet to do anything about the cornucopia of options? When Haskell began, there were many <em>similar</em> options; the list above is heterogeneous. Is that because it's too early in to tell what the Right choices will be? Is this problem fundamentally harder than the one that inspired the Haskell precursors?
<p>
I'm not sure, though deciding how to ensure termination seems particularly tricky. Nonetheless, there are other decisions that aren't as directly related to the central dependent type issues, like syntax, functional purity (though this is related to termination), and editing environment. Maybe these issues will divide the ecosystem into a few niches, each dominated by one player. In the meantime, it's tough to choose.http://blog.jbapple.com/2007/12/common-language-for-dependently-typed.htmlnoreply@blogger.com (Jim Apple)9tag:blogger.com,1999:blog-6839602.post-8255962414155147935Sat, 10 Nov 2007 02:11:00 +00002007-11-09T21:12:08.593-08:00Heyting algebraLectures on the Curry-Howard Isomorphism saves the day<a href="http://www.diku.dk/~rambo/">Morten Heine B. Sørensen</a> and <a href="http://www.mimuw.edu.pl/~urzy/">Pawel Urzyczyn</a>'s <a href="http://citeseer.ist.psu.edu/519604.html"><cite>Lectures on the Curry-Howard Isomorphism</cite></a> (<a href="http://folli.loria.fr/cds/1999/library/pdf/curry-howard.pdf">mirror 1</a>, <a href="ftp://ftp.mimuw.edu.pl/People/urzy/ch.ps.gz">mirror 2</a>, <a href="ftp://ftp.mimuw.edu.pl/People/urzy/errata127.ps.gz">errata</a>) provides answers to two questions I asked here before:
<p>
<a href="http://blog.jbapple.com/2007/08/are-there-any-zero-knowledge-proofs.html">I speculated about a complexity problem and its relation to types</a>. On page 104 of LotCHI (92, in print), the authors note that, in the simply-typed lambda calculus, a reduction of the type inhabitation problem to the type checking problem would show that P = PSPACE.
<p>
<a href="http://blog.jbapple.com/2007/08/leibniz-equality-decomposition-and.html">I also wondered if there was a Heyting algebra for higher-order polymorphic typed lambda calculi that we can use to show that some type is uninhabited</a>. LotCHI section 12.2 gets part of the way there (The authors cover F2, I would need F3, I think.), with the answer that yes, there is such an algebra, but no, it doesn't make things so easy.http://blog.jbapple.com/2007/11/lectures-on-curry-howard-isomorphism.htmlnoreply@blogger.com (Jim Apple)0tag:blogger.com,1999:blog-6839602.post-7023054184215987116Wed, 05 Sep 2007 02:17:00 +00002008-03-23T16:43:16.935-07:00constructive logicfuzzy logicFuzzy Logic and Inuitionistic Logic<p>
I recently got rid of a pop science book on <a href="http://en.wikipedia.org/wiki/Fuzzy_logic">fuzzy logic</a> that I purchased about eight years ago. When I first read it, it seemed to me to be not all that interesting, since it didn't seem like it created any particularly new ways of thinking about things. After all, calling someone "tall" is just shorthand, and it's not exactly revolutionary to call someone "somewhat tall" or "48% tall", since we can do that already when we talk about any continuous domain.
<p>
I put the book aside and figured that I either didn't get it, I had picked a bad explanation, or it truly was not something I would be interested in.
<p>
It occurs to me now that the idea of indeterminate truth should be very interesting to me, since I'm interested in intuitionistic logic, especially where provability differs from truth. The <a href="http://plato.stanford.edu/">Stanford Encyclopedia of Philosophy</a> <a href="http://plato.stanford.edu/entries/logic-fuzzy/">indicates that the fuzzy logic I was thinking of is the "broad sense" or "fuzzy control", and that there's a whole other sense of fuzzy logic that is more closely related to my interests.</a>http://blog.jbapple.com/2007/09/fuzzy-logic-and-inuitionistic-logic.htmlnoreply@blogger.com (Jim Apple)0tag:blogger.com,1999:blog-6839602.post-6808416011239950610Wed, 05 Sep 2007 02:16:00 +00002007-09-04T22:19:16.686-07:00zero-knowledge proofAre there any Zero-Knowledge Proofs?<a href="http://blog.jbapple.com/2007/02/existentials-and-zero-knowledge-proofs.html">I speculated before about zero-knowledge proofs and existentials</a>. What I had in mind was encoding knowledge hiding via types. I suspect this result would be more interesting than I had imagined. Here is my understanding:
<p>
Zero-knowledge proofs are interactive proofs, and are therefore in the class <a href="http://en.wikipedia.org/wiki/IP_%28complexity%29">IP</a>. This class is the same as <a href="http://en.wikipedia.org/wiki/PSPACE">PSPACE</a>, which is not yet known to be distinct from P (though it certainly contains P). So, it's possible that P = IP = PSPACE, and ZK proofs can't hide anything the verifier couldn't calculate herself. In other words, we may one day discover that most of our ZK proof protocols are useless. (This is not the whole story, as there are lots of variations on interactive proving.)
<p>
So, if there were a correspondence between these ZK proofs and existential types, it would either settle the P = PSPACE problem or discover a problem in type theory that is equivalent to it.
<p>
Each of these seems quite unlikely to me.
<p>
<a href="http://www.infsec.cs.uni-sb.de/~maffei/ResTeach.html">There is at least one person, however, who is doing research about the relationship between types and cryptography.</a>http://blog.jbapple.com/2007/08/are-there-any-zero-knowledge-proofs.htmlnoreply@blogger.com (Jim Apple)1tag:blogger.com,1999:blog-6839602.post-1538703260125065458Tue, 28 Aug 2007 14:49:00 +00002007-08-28T09:21:35.884-07:00cardinal numbersNaming Large Integers is Naming Strong LogicsScott Aaronson's <a href="http://www.scottaaronson.com/writings/bignumbers.html">Who Can Name the Bigger Number?</a> was <a href="http://programming.reddit.com/info/2jbud/comments">recently discussed on the programming subreddit</a>. One of the comments noted the <a href="http://web.mit.edu/arayo/www/bignums.html">Big Number Duel</a>, which was inspired by Aaronson's article. The winning entry in the duel was
<blockquote>
The smallest number bigger than any finite number named by an expression in the language of set theory with a googol symbols or less.
</blockquote>
I think we can do a little bit better without increasing from 10<sup>100</sup> the number of symbols allowed:
<blockquote>
The smallest number bigger than any finite number named by an expression in the language of set theory <em>plus an axiom stating the existence of a proper class of <a href="http://en.wikipedia.org/wiki/Inaccessible_cardinal">inaccessible cardinals</a></em> with a googol symbols or less.
</blockquote>
<p>
Since this theory (<a href="http://en.wikipedia.org/wiki/ZFC">ZFC</a>+class of inaccessibles) is stronger than ZFC by itself, I suspect it will define larger integers in the same number of symbols. We could continue along this track by listing <a href="http://en.wikipedia.org/wiki/List_of_large_cardinal_properties">larger cardinals</a> and <a href="http://en.wikipedia.org/wiki/Category:Axioms_of_set_theory">stronger axioms of set theory</a>. This game now becomes essentially Bram Cohen's <a href="http://bitconjurer.org/minefield.html">MineField</a>, in which we are not naming just numbers, but logics.
<p>
Besides the Big Number Duel, another test of the "name large integers" game was the <a href="http://djm.cc/dmoews.html">C Bignum Bakeoff</a>, which asked contestants to wite a C program that returned a large number. Ralph Loader won by to shoehorning a logic called the Calculus of Constructions into his entry, then simply saying something like "the largest integer definable in the Calculus of Constructions using less than a googol symbols".
<p>
The idea of naming finite numbers by extending the strength of not only the working notation but also the working logic is not new; see <a href="http://en.wikipedia.org/wiki/Zero_sharp">0<sup>#</sup></a> and <a href="http://en.wikipedia.org/wiki/Zero_dagger">0<sup>†</sup></a>.http://blog.jbapple.com/2007/08/naming-large-integers-is-naming-strong.htmlnoreply@blogger.com (Jim Apple)0tag:blogger.com,1999:blog-6839602.post-6687997688298412079Thu, 23 Aug 2007 13:42:00 +00002008-01-22T20:49:12.145-08:00grammar checkinglaypeoplestatic analysisStatic Analysis as Grammar Checking<p>
When I explain what I intend to study to friends who don't program, I say something like the text below. I'm still working out the kinks in the analogy, but this is my starting point:
</p>
<hr/>
<p>
When we write, we sometimes make mistakes:
<blockquote>
I am hunry when I wake up.
</blockquote>
So we invented spelling checkers to catch this simple mistake. We did the same thing for computer languages a long time ago, to catch simple mistakes like spelling errors. And, just as we then invented grammar checkers to catch sentences like:
<blockquote>
I am hungrily when I wake up.
</blockquote>
that spelling checkers wouldn't catch, we also invented more sophisticated methods to catch more sophisticated mistakes in computer programs.
</p>
<p>
But grammar rules can sometimes restrict how expressive our sentences are if we wish to speak informally, or to be funny or poetic, or to quote someone famous:
<blockquote>
You've got a friend in Pennsylvania.<br/>
What price justice?<br/>
Hand me a hypodeemic nerdle.
</blockquote>
For computer programs, we try to characterize useful patterns (like "rhetorical question" or "implicit subject in imperative" in English) and build sets of rules called <em>type systems</em>. These sets of rules are designed to allow these patterns without allowing incorrect constructions. Type systems require all incorrect constructions to be corrected by the author before a program is run.
</p>
<p>At the same time, we can build more permissive tools that look for particular patterns that are likely to be errors, like <a href="http://www.uic.edu/com/eye/LearningAboutVision/EyeSite/OpticalIllustions/Paris.shtml">repeated words</a> or a lowercase letter following a question mark. Anything flagged by the tool as possibly erroneous can be inspected by the author and corrected if necessary.
</p>
<p>
The goal of all of this work (called <em>static analysis</em>) is to catch bugs in software before it is shipped and <a href="http://video.google.com/videosearch?q=ellen+feiss">bothers users</a> or <a href="http://en.wikipedia.org/wiki/Ariane_5_Flight_501">blows up aerospace equipment</a>. <!-- or <a href="http://en.wikipedia.org/wiki/Therac-25">kills cancer patients</a> -->
</p>
<p>
My goal is to build new static analysis tools to help prevent rocket explosions and Mac commercials.
</p>http://blog.jbapple.com/2007/08/static-analysis-as-grammar-checking.htmlnoreply@blogger.com (Jim Apple)0tag:blogger.com,1999:blog-6839602.post-8690048312906662507Wed, 22 Aug 2007 18:12:00 +00002008-03-23T16:29:28.621-07:00Heyting algebraLeibniz equalityLeibniz Equality, Decomposition, and Definability<p>
In any <a href="http://en.wikipedia.org/wiki/Robinson_arithmetic_Q#Metamathematics">interesting logic</a>, <a href="http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems">there are propositions which are true but not provable</a>. The same goes for <a href="http://plato.stanford.edu/entries/logic-intuitionistic/">intuitionistic logic</a>. By the <a href="http://en.wikipedia.org/wiki/Curry-Howard_isomorphism">Curry-Howard correspondence</a>, there are types for which neither the types themselves nor their negations are inhabited in the typed lambda calculus. An example of this is <a href="http://en.wikipedia.org/wiki/Peirce's_law">Peirce's law</a>: <code>∀ p, q . ((p -> q) -> p) -> p</code>. We can <a href="http://en.wikipedia.org/wiki/Heyting_algebra#Heyting_algebras_as_applied_to_intuitionistic_logic">use Heyting algebra to show that Peirce's law is not provable in intuitionistic logic</a>. According to John C. Mitchell's <cite>Foundations for Programming Languages</cite>, problem 4.3.16, we could also show that this is not provable because:
<blockquote>
. . . if there us a closed lambda term M:((a -> b) -> a) -> a then there is a closed normal form (the normal form of M) of this type. Show that this implicational formula is not provable by showing there is no closed normal form term of this type.
</blockquote>
</p>
<p>
In <a href="http://homepage.mac.com/pasalic/p2/">Emir Pasalic</a>'s <a href="http://homepage.mac.com/pasalic/p2/papers/thesis.pdf">PhD thesis</a>, (end of section 4.2.2, page 80 in the PDF, 70 in print), he mentions that it is unknown whether the following type is inhabited:
<pre>
∀ a, b, c, d . Equal (a,b) (c,d) -> Equal a c
</pre>
where type equality is defined by Leibniz equality
<pre>
data Equal a b = Equal (∀ f . f a -> f b)
</pre>
To avoid dealing with datatypes or pairs, this can be expanded to
<pre>
∀ a, b, c, d .
(∀ f . f (∀ r . (a -> b -> r) -> r) -> f (∀ s . (c -> d -> s) -> s))
->
(∀ g . g a -> g c)
</pre>
In <a href="http://www.comp.nus.edu.sg/~sulzmann/manuscript/gadtless.ps">GADTless Programming in Haskell 98</a> (Section 6, top of page 13) <a href="http://www.comp.nus.edu.sg/~sulzmann/">Martin Sulzmann</a> and <a href="http://users.ox.ac.uk/~wolf2335/">Meng Wang</a> call this the decomposition law.
</p>
<p>
Is there some Heyting algebra for higher-order polymorphic typed lambda calculi that we can use to show that this type is uninhabited?
</p>http://blog.jbapple.com/2007/08/leibniz-equality-decomposition-and.htmlnoreply@blogger.com (Jim Apple)13tag:blogger.com,1999:blog-6839602.post-7625667769896283845Wed, 25 Jul 2007 03:51:00 +00002008-03-23T16:36:22.361-07:00Haskellordinalsε0 in an Ord instanceIn <a href="http://blog.jbapple.com/2007/07/ord-countable-ordinals-and-idea-of.html" >my last post</a>, I worked rather hard to approach ε<sub>0</sub>, but there is a much simpler way to form a type with an <code>Ord</code> instance that has order type ε<sub>0</sub>, according to <a href="http://citeseer.ist.psu.edu/131185.html" >Trees, Ordinals and Termination</a> (<a href="http://www.math.tau.ac.il/~nachumd/papers/caap-revised.ps.gz" >mirror</a>)
<pre>
import List
data Tree = Node | Tree [Tree]
instance Ord Tree where
compare Node Node = EQ
compare Node (Tree _) = LT
compare (Tree _) Node = GT
compare (Tree x) (Tree y) = compare (sort x) (sort y)
instance Eq Tree where
x == y = compare x y == EQ
</pre>
Or, according to <a href="http://www.math.tau.ac.il/~nachumd/papers/ordinals-new.ps.gz" >Ordinal Arithmetic with List Structures</a> (<a href="http://citeseer.ist.psu.edu/168717.html" >mirror</a>)
<pre>
data Cons = Nil | Cons Cons Cons
instance Ord Cons where
compare Nil Nil = EQ
compare Nil (Cons _ _) = LT
compare (Cons _ _) Nil = GT
compare a@(Cons x' y') b@(Cons x y) =
case compare x' x of
LT -> compare y' b
EQ -> compare y' y
GT -> compare a y
instance Eq Cons where
x == y = compare x y == EQ
</pre>
These representations do not help in the general problem of representing all ordinals less than some ordinal κ, but they are much simpler than our previous method.
<p>
For trees with larger order types, see <a href="http://repository.upenn.edu/cis_reports/238/" >What's so special about Kruskal's theorem and the ordinal &Gamma<sub>0</sub></a> (<a href="http://www.cis.upenn.edu/~jean/gallier-old-pubs.html" >mirror</a>)http://blog.jbapple.com/2007/07/0-in-ord-instance.htmlnoreply@blogger.com (Jim Apple)0tag:blogger.com,1999:blog-6839602.post-4451561834519323384Tue, 24 Jul 2007 01:30:00 +00002008-03-23T16:37:25.921-07:00ordinalsOrd, Countable Ordinals, and an Idea of sigfpe<p>
This post is literate Haskell.
<p>
In the comments on my last post about ordinals, <a
href="http://www.blogger.com/profile/08096190433222340957">sigfpe</a>
<a
href="http://blog.jbapple.com/2007/07/ordinal-notation-and-computer-proof.html#c2460833816539219994">
suggests</a> the following type constructors:
<pre>
type One = ()
type Two = Either One One
type N = [One]
type Nplus1 = Either N One
type NplusN = Either N N
type NtimesN = (N,N)
type NpowN = [N]
type NpowNplusN = Either NpowN N
</pre>
<p>
The idea is that each of these has an <code>Ord</code> instance
defined. I think he's suggesting that the <code>Ord</code> instance
for each (ignoring _|_) has an order type that is the same as the
ordinal its name corresponds to. I have some quibbles with his
implementation, but I really like the idea, and so I'll expand on it
below.
<p>
I'll start with my disagreements. My first is with the order for
<code>NpowN</code>. In NpowN
<pre>
[[(),()]] > [[()],[(),()]] > [[()],[()],[(),()]] > . . .
</pre>
<p>
or in simpler form
<pre>
[2] > [1,2] > [1,1,2] > . . .
</pre>
<p>
Since no ordinal has an infinite decreasing sequence, the order type
of <code>[N]</code> is not that of an ordinal. For now, we'll just
disregard the <code>[]</code> type constructor.
<p>
My second quibble is with <code>Times</code>. sigfpe does not make
this explicit, but the inference I drew from his examples was that we
could define <code>Times</code> as
<pre>
type Times = (,)
</pre>
<p>
That doesn't quite work, though. <a
href="http://en.wikipedia.org/wiki/Ordinal_arithmetic#Multiplication">Ordinal
arithmetic</a> places the least significant part first, but the
<code>Ord</code> instance for <code>(,)</code> places the most
significant part first.
<p>
Now that we have these differences out of the way, let's get to the code.
<p>
We'll need these options for type class machinery later.
<pre>
> {-# OPTIONS -fglasgow-exts #-}
> {-# OPTIONS -fallow-incoherent-instances #-}
</pre>
<p>
Ala sigfpe:
<pre>
> type One = ()
> type Plus = Either
> type Times = Flip Both
>
> data Both a b = Both a b
> newtype Flip f a b = Flip (f b a)
</pre>
<p>
To define <code>Times</code>, we use a pair datatype with the standard
Haskell ordering (see <code>instance Ordinal2 Both</code> below), but
apply the newtype <code>Flip</code>, which warrants its own
definition, as it will be useful elsewhere.
<p>
So far, we can only define finite ordinals. In order to represent
larger ordinals, we want to be able to represent an unlimited number
of applications of a type constructor to a type.
<pre>
> data ApplyN f x = More (ApplyN f (f x))
> | Stop x
</pre>
<p>
<code>ApplyN</code> does this -- after n applications of
<code>More</code>, the type <code>x</code> is wrapped n times in the
type constructor <code>f</code>. Essentially, <code>ApplyN f x</code>
is f<sup>ω</sup>(x).
<p>
Our first example of this will be adding one ω times.
<pre>
> type N = ApplyN (Flip Plus One) One
</pre>
<p>
<!--
I'll explain the reason for the <code>Flip</code> later. For now, this
should look like (λ x . x + 1)<sup>ω</sup> (1).
-->
This should look like (λ x . x + 1)<sup>ω</sup> (1).
<p>
If <code>ApplyN</code> works as advertized, <code>N</code> should have
order type ω under a naive definition of
<code>Ord</code>. Unfortunately, it does not. First of all, we can't
automatically derive <code>Ord</code> for the type
<code>ApplyN</code>, since it uses a type constructor, <code>f</code>,
to build a new parameter. We will need
<pre>
> class Ordinal1 f where
> comp1 :: Ordinal a => f a -> f a -> Ordering
</pre>
<p>
to describe the contract <code>f</code> must meet to make <code>ApplyN
f x</code> ordered. Note that we use the class <code>Ordinal</code>
here, which is used only to avoid messing the with <code>Eq</code>
requirement on instances for <code>Ord</code>.
<pre>
> class Ordinal t where
> comp :: t -> t -> Ordering
</pre>
<p>
The second problem with the naive instance of <code>Ordinal</code> on
<code>ApplyN</code> is that each application of <code>More</code>
leads to a new type closer to the type we're really talking
about. What I mean by this is that, for the case of <code>N</code>, we
really want to talk about
<pre>
Flip Plus One (Flip Plus One (Flip Plus One . . . .
</pre>
<p>
Which we can't directly say in Haskell.
<p>
We want to be talking about the type that is the limit. Since we can't
do that, to compare two values, we'll compare them at the maximum of
their levels. For instance, if we want to compare the values <code>Stop
()</code> and <code> More $ More $ Stop $ Flip $ Left $ Flip $ Left
()</code>, both of which are of type <code>N</code>, we'll inject the
value <code>()</code> into the higher level. To do this, we also need
<code>f</code> to be have the property that we can inject into it a
value of its type parameter.
<pre>
> class Container f where
> inject :: x -> f x
</pre>
<p>
To bring this back to the ordinals, we'll be representing
ω<sup>ω</sup> as either and ordinal less than ω, or an
ordinal less than ω<sup>2</sup>, or an ordinal less than
ω<sup>3</sup> or …, and to compare two ordinals, we get a
representation of each in a common level, then compare them using the
comparison for ordinals less than the limiting ordinal of that level.
<pre>
> instance (Container f, Ordinal1 f) => Ordinal1 (ApplyN f) where
> comp1 (Stop u) (Stop v) = comp u v
> comp1 (Stop u) (More v) = comp (Stop (inject u)) v
> comp1 (More u) (Stop v) = comp u (Stop (inject v))
> comp1 (More u) (More v) = comp1 u v
</pre>
<p>
We've defined the ordering on <code>ApplyN f</code> so that
<pre>
comp (Stop x) (More (Stop (inject x))) == EQ
</pre>
<p>
which is what the paragraph above says, but more concise. We've
defined an equivalence relation on values of the type <code>ApplyN f
t</code> such that <code>x == inject x</code>, so we're off to a good
start.
<p>
We'll also want <code>inject</code> to be monotone, that is
<pre>
x < y ==> inject x < inject y
</pre>
<p>
and for <code>inject</code> to send the order type of the domain not
just to <em>some</em> order in the codomain, but to the initial order
in the codomain. So, it's easy to write
<pre>
> injectPlusL :: a -> Plus a b
> injectPlusL x = Left x
</pre>
<p>
or
<pre>
> instance Container (Flip Plus b) where
> inject v = Flip (Left v)
</pre>
<p>
Injecting a into a*b is trickier, since we need the second part of the
pair to be the minimal possible value in order for the injection range
to be the initial part of the order. For this we define
<pre>
> class Least x where
> least :: x
> instance Least One where
> least = ()
> instance Least a => Least (Plus a b) where
> least = Left least
> instance (Least a, Least b) => Least (Times a b) where
> least = Flip (Both least least)
> instance Least b => Least (Flip Plus a b) where
> least = Flip (Left least)
> instance (Least a, Least b) => Least (Flip Times a b) where
> least = Flip (Flip (Both least least))
> instance Least x => Least (ApplyN f x) where
> least = Stop least
</pre>
<p>
And we can now write the injection from a to a*b:
<pre>
> instance (Least a) => Container (Flip Times a) where
> inject v = Flip (Flip (Both least v))
</pre>
<p>
We also have the trivial
<pre>
> instance Container (ApplyN f) where
> inject x = Stop x
</pre>
<p>
Let's write the base instances for Ordinal in as general a way as possible:
<pre>
> class Ordinal2 f where
> comp2 :: (Ordinal a, Ordinal b) => f a b -> f a b -> Ordering
> instance Ordinal2 Plus where
> comp2 (Left _) (Right _) = LT
> comp2 (Right _) (Left _) = GT
> comp2 (Left x) (Left y) = comp x y
> comp2 (Right x) (Right y) = comp x y
> instance Ordinal2 Both where
> comp2 (Both p q) (Both x y) =
> case comp p x of
> LT -> LT
> GT -> GT
> EQ -> comp q y
> instance Ordinal2 f => Ordinal2 (Flip f) where
> comp2 (Flip x) (Flip y) = comp2 x y
>
> instance Ordinal () where
> comp _ _ = EQ
</pre>
<p>
And the conversion instances between the n-ary Ordinal instances:
<pre>
> instance (Ordinal1 f, Ordinal a) => Ordinal (f a) where
> comp = comp1
> instance (Ordinal2 f, Ordinal a, Ordinal b) => Ordinal (f a b) where
> comp = comp2
> instance (Ordinal2 f, Ordinal a) => Ordinal1 (f a) where
> comp1 = comp2
</pre>
<p>
Now let's do some examples. First we check that <code>Ordinal</code> is
defined for <code>N</code>:
<pre>
> n_ok = comp (undefined :: N) (undefined :: N)
</pre>
<p>
ω<sup>ω</sup>:
<pre>
> type NpowN = ApplyN (Flip Times N) One
> npowN_ok = comp (undefined :: NpowN) (undefined :: NpowN)
</pre>
<p>
We can now plug in <code>NpowN</code> into its own definition to get
ω<sup>ω</sup> * ω = ω<sup>ω + 1</sup>
<pre>
> type NpowNplusOne = ApplyN (Flip Times N) NpowN
> nPowNplusOne_ok = comp (undefined :: NpowNplusOne) (undefined :: NpowNplusOne)
</pre>
or ω<sup>ω * ω</sup> =
ω<sup>ω<sup>2</sup></sup>:
<pre>
> type NpowNpow2 = ApplyN (Flip Times NpowN) One
> npowNpow2_ok = comp (undefined :: NpowNpow2) (undefined :: NpowNpow2)
</pre>
<p>
The second method looks more powerful, but continuing it keeps us
below ω<sup>ω<sup>&omega</sup></sup>, so let's use the
first method of substituting back in to see if we can get further.
<p>
ω<sup>ω + 2</sup>:
<pre>
> type NpowNplus2 = ApplyN (Flip Times N) NpowNplusOne
> nPowNplus2_ok = comp (undefined :: NpowNplus2) (undefined :: NpowNplus2)
</pre>
<p>
We can now plug <code>ApplyN</code> back into itself, and extend this
to ω<sup>ω + &omega</sup> = ω<sup>ω * 2</sup>:
<pre>
> type NpowNtimes2 = ApplyN (ApplyN (Flip Times N)) One
> npowNtimes2_ok = comp (undefined :: NpowNtimes2) (undefined :: NpowNtimes2)
</pre>
<p>
Similarly, ω<sup>ω * 3</sup>:
<pre>
> type NpowNtimes3 = ApplyN (ApplyN (Flip Times N)) NpowNtimes2
> npowNtimes3_ok = comp (undefined :: NpowNtimes3) (undefined :: NpowNtimes3)
</pre>
<p>
ω<sup>ω * ω</sup> =
ω<sup>ω<sup>2</sup></sup>, which we apready saw before,
can also be written as
<pre>
> type NpowNpow2' = ApplyN (ApplyN (ApplyN (Flip Times N))) One
> npowNpow2'_ok = comp (undefined :: NpowNpow2') (undefined :: NpowNpow2')
</pre>
<p>
ω<sup>ω<sup>2</sup> * ω</sup> = ω<sup>ω<sup>3</sup></sup> =
<pre>
> type NpowNpow3 = ApplyN (ApplyN (ApplyN (Flip Times N))) NpowNpow2
> npowNpow3_ok = comp (undefined :: NpowNpow3) (undefined :: NpowNpow3)
</pre>
<p>
ω<sup>ω<sup>ω</sup></sup>:
<pre>
> type NpowNpowN = ApplyN (ApplyN (ApplyN (ApplyN (Flip Times N)))) One
> npowNpowN_ok = comp (undefined :: NpowNpowN) (undefined :: NpowNpowN)
</pre>
<p>
ω<sup>ω<sup>ω + 1</sup></sup>:
<pre>
> type NpowNpowNplusOne = ApplyN (ApplyN (ApplyN (ApplyN (Flip Times N)))) NpowNpowN
> npowNpowNplusOne_ok = comp (undefined :: NpowNpowNplusOne) (undefined :: NpowNpowNplusOne)
</pre>
<p>
We can continue this process up to, but not including,
ε<sub>0</sub>. We might be able to go further than this, but
I'll save that for later.
<p>
Thanks to sigfpe for the idea!http://blog.jbapple.com/2007/07/ord-countable-ordinals-and-idea-of.htmlnoreply@blogger.com (Jim Apple)3tag:blogger.com,1999:blog-6839602.post-7868504782448649445Sat, 21 Jul 2007 03:19:00 +00002008-03-23T16:35:45.763-07:00CoqordinalsOrdinal Notation and Computer Proof<p>
<a href="http://blog.jbapple.com/2007/06/ordinals-part-2.html" >Last ordinal post here</a>
</p>
<p>
<a href="http://coq.inria.fr/contribs/Cantor.html" >There is an implementation in Coq of the countable ordinals up to Γ<sub>0</sub></a>.
</p>http://blog.jbapple.com/2007/07/ordinal-notation-and-computer-proof.htmlnoreply@blogger.com (Jim Apple)2tag:blogger.com,1999:blog-6839602.post-3751056714695966153Fri, 20 Jul 2007 21:55:00 +00002008-03-23T16:42:18.939-07:00Coqreferential transparencyMore Proof of Referential Transparency<p>
<a href="http://blog.jbapple.com/2007/06/proof-of-referential-transparency.html" >Previously, I talked about proving referential transparency</a>. The authors of <a href="http://www.lri.fr/~filliatr/puf/index.en.html" >A Persistent Union-Find Data Structure</a> (<a href="http://www.lri.fr/~filliatr/ftp/publis/puf-wml07.ps" >other version</a>) use <a href="http://coq.inria.fr/" >Coq</a> to prove imperative functions referentially transparent, and they point out the work of <a href="http://home.pipeline.com/~hbaker1/" >Harold Baker</a>, who designed <a href="http://citeseer.ist.psu.edu/245043.html" >fast persistent arrays</a> (<a href="http://citeseer.ist.psu.edu/250000.html" >and here</a>), which they also prove to be referentially transparent. <a href="http://www.haskell.org/ghc/docs/6.8.2/html/libraries/array/Data-Array-Diff.html">These arrays are even available in Haskell</a>, though wrapped in the IO monad.
</p>
<p>
The authors of the union-find paper say that their structure is not "purely applicative". I don't actually know what that means, but I suppose it means it's not strictly functional, since it requires in-place modification.
</p>
<p>
In any case, there are now at least four cases for being able to prove referential transparency so we can use it without wrapping everything in the IO monad:
<ul>
<li> Memoization - <a href="http://research.microsoft.com/Users/simonpj/Papers/weak.htm" >For memoization in (not just for) Haskell, see this paper by the Simons and Conal Elliott.</a> (<a href="http://citeseer.ist.psu.edu/peytonjones99stretching.html" >mirror 1</a>, <a href="http://conal.net/papers/weak.ps" >mirror 2</a>)
<li> Diff Arrays
<li> Splay Trees
<li> Union-Find
</ul>
Any other ideas?
</p>http://blog.jbapple.com/2007/07/more-proof-of-referential-transparency.htmlnoreply@blogger.com (Jim Apple)0tag:blogger.com,1999:blog-6839602.post-2078216538647453280Sat, 30 Jun 2007 16:02:00 +00002008-03-23T16:32:15.639-07:00constructive logiccountabilityordinalsV=LConstructability, Uncountability, and ω-Haskell<p>
<a href="http://japple.blogspot.com/2007/06/ordinals-part-2.html">My last post about the uncountable ordinals</a> <a href="http://programming.reddit.com/info/22e5n/comments">ended up on the programming subreddit</a>, where <a href="http://programming.reddit.com/user/augustss">someone who I think is Lennart Augustsson</a> <a href="http://programming.reddit.com/info/22e5n/comments/c22f2w">said</a>:
<blockquote>
Wow, I didn't realize you could do this. Now I have to wrap my brain around in what sense you can represent uncountable ordinals in Haskell since there are only a countable number of Haskell programs. It must be something like constructive reals...
</blockquote>
</p>
<p>
I think he's exactly right, and I think it has something to do with <a href="http://en.wikipedia.org/wiki/V=L">V=L</a>, models, and <a href="http://japple.blogspot.com/2007/02/definability-and-continuity.html">how many functions are definable in Haskell</a>. I'm going out of my comfort zone on this, so please correct me if I make any incorrect or nonsensical statements. I'll use as my example the powerset of the natural numbers, which is certainly uncountable, and already definable in Haskell with
<pre>
data Nat = Z | S Nat
type Powerset t = t -> Bool
</pre>
</p>
<p>
From the viewpoint of ZFC, there are an uncountable number of ZFC functions from the natural numbers to the booleans. From the viewpoint of Haskell, there are an uncountable number of Haskell functions from the natural numbers to the booleans. But, from the world of ZFC, the number of Haskell functions from the natural numbers to the booleans is countable: we can simply order them by their definitions lexicographically. Since every function definable in Haskell has a finite definition and the cardinality of a countable union of finite sets is countable, the function definitions of type <code>Nat -> Bool</code> are countable.
</p>
<div align="center">
|{f : f <- (<b>N</b> -> 2)<sub>ZFC</sub>}| ><sub>ZFC</sub> |<b>N</b>|<br>
|{f : f <- (<b>N</b> -> 2)<sub>Haskell</sub>}| ><sub>Haskell</sub> |<b>N</b>|<br>
|{f : f <- (<b>N</b> -> 2)<sub>Haskell</sub>}| =<sub>ZFC</sub> Σ<sub>n <- <b>N</b></sub> |all n-bit functions from <b>N</b> -> Bool| = |<b>N</b>|<br>
</div>
<p>
From the viewpoint of Haskell, though, this can't be proven; functions are opaque, so we have no way to order or count them. This might not be true if we use some of the unsafe features of Haskell that would allow us to look at the actual assembly corresponding to a function.
</p>
<p>
We could, I suppose, imagine a programming language which was not limited to finite-length function definitions. ω-Haskell would not only have types with seemingly uncountable numbers of inhabitants, but each inhabitant would also be definable. Yuk!
</p>http://blog.jbapple.com/2007/06/constructability-uncountability-and.htmlnoreply@blogger.com (Jim Apple)5tag:blogger.com,1999:blog-6839602.post-5839509165539293360Sat, 30 Jun 2007 15:47:00 +00002008-03-23T16:39:48.421-07:00effect inferenceeffectsRegion, Effect and Closure Inference, Part 2<p>
<a href="http://japple.blogspot.com/2007/06/proof-of-referential-transparency.html">Part 1</a>
</p>
<p>
<a href="http://www.blogger.com/profile/05322254915965832369">Michael Stone</a> was correct in his comments to part 1. Ben Lippmeier elaborated to me in an email:
<blockquote>
In those slides,
<br>
(%) is the kind of regions.<br>
(!) is the kind of effects.<br>
($) is the kind of closures.<br>
<br>
The symbol represents the kind, as well as the name space of the R/E/C variables.
<br>
…
<br>
I don't have a paper for this stuff at the moment, it's still under development - but the type system is based on some other work that has been around for a while:
<br>
The Type and Effect Discipline<br>
Jean-Pierre Talpin, Pierre Jouvelot<br>
<br>
Polymorphic Type, Region and Effect Inference<br>
Jean-Pierre Talpin, Pierre Jouvelot<br>
<br>
Polymorphic type inference and assignment<br>
(For the closure typing)<br>
Xavier Leroy<br>
<br>
The type system is a merge of the ones described in the above two papers, but with some extra stuff added on to make it practical to use in a real compiler.
</blockquote>
</p>http://blog.jbapple.com/2007/06/region-effect-and-closure-inference.htmlnoreply@blogger.com (Jim Apple)0tag:blogger.com,1999:blog-6839602.post-2544858816282384802Sat, 30 Jun 2007 00:56:00 +00002008-03-23T16:52:42.680-07:00countabilityordinalsOrdinals, part 2<p>
<a href="http://japple.blogspot.com/2007/02/countable-ordinals-in-haskell.html">Part 1</a>
</p>
<p>
<a href="http://homepages.inf.ed.ac.uk/v1phanc1/">Peter G. Hancock</a> <a href="http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=66">reminded us of the obvious way to define uncountable ordinals</a>. A rough translation into a single data type, rather than a family:
<pre>
data Ordinal n = Zero (Nat n)
| Succ (Ordinal n)
| forall t . Limit (Less t n) (Ordinal t -> Ordinal n)
</pre>
The parameter <code>n</code> is the "class" of the ordinal. We need the helper definitions:
<pre>
data Nat n where
Z :: Nat Z
S :: Nat n -> Nat (S n)
data Z
data S n
data Less a b where
LessZ :: Nat b -> Less Z (S b)
LessS :: Less a b -> Less (S a) (S b)
embed :: Ordinal n -> Ordinal (S n)
embed (Zero x) = Zero (S x)
embed (Succ x) = Succ (embed x)
embed (Limit e f) = Limit (onemore e) (embed . f)
where
onemore :: Less a b -> Less a (S b)
onemore (LessZ x) = LessZ (S x)
onemore (LessS p) = LessS (onemore p)
</pre>
Then we can define the first uncountable ordinal as
<pre>
omega_1 = Limit (LessS (LessZ Z)) embed
</pre>
and the sequence of ωs up to ω<sub>ω</sub> as
<pre>
omega_n :: Nat n -> Ordinal n
omega_n Z = Zero Z
omega_n (S n) = Limit (plusone n) embed
where
plusone :: Nat n -> Less n (S n)
plusone Z = LessZ Z
plusone (S n) = LessS (plusone n)
</pre>
<p>
Hancock has <a href="http://homepages.inf.ed.ac.uk/v1phanc1/chat.html">many other interesting ways to represent ordinals</a>, including <a href="http://homepages.inf.ed.ac.uk/v1phanc1/conway.html">as surreal numbers</a> (<a href="http://homepages.inf.ed.ac.uk/v1phanc1/Conway.lhs">with code</a>), in which we can provide a more precise answer the the question I was originally responding to, <a href="http://www.randomhacks.net/articles/2007/02/02/divide-infinity-by-2">What happens when you divide infinite by two?</a> In the case of surreal numbers, you get, simply, ω/2, just as you do with the <a href="http://en.wikipedia.org/wiki/Hyperreal_number">hyperreals</a>. Hancock also provides a datatype for the ordinals up to Γ<sub>0</sub> without resorting to embedded functions, which means we can do things like <a href="http://en.wikipedia.org/wiki/Large_countable_ordinals#Predicative_definitions_and_the_Veblen_hierarchy">computably compare them</a>.
</p>http://blog.jbapple.com/2007/06/ordinals-part-2.htmlnoreply@blogger.com (Jim Apple)0tag:blogger.com,1999:blog-6839602.post-4238148025277585507Sun, 24 Jun 2007 03:58:00 +00002008-03-23T16:39:17.652-07:00effectsquotient typesreferential transparencyCompiler Proof of Referential Transparency<p>
Programs in languages with mutation can make optimizations that Haskell programs can't, at least not without compiler magic, unsafePerformIO, or wrapping return types in the IO monad. Simple examples that spring to mind are memoization and <a href="http://en.wikipedia.org/wiki/Splay_tree">splay trees</a>. Here, operations that should have no semantic effects (calling a <code>fib</code> function or doing a <code>find</code> on a splay map) do have actual effects. It would be nice if Haskell programmers could write these optimizations and prove them safe with the type system, then use these functions as if they were referentially transparent.
</p>
<p>
My idea for this a few months ago was to use quotient types, since quotient types equate two actually different things that are functionally the same under some view. A Fibonacci function with a memoization table up to 100 looks the same to a caller as one with no memoized values at all, so they are equal under some quotient.
</p>
<p>
Other things came up, and I put off this idea for a while, and I have now seen a really cool way for Haskell programmers to deal with local effects. <a href="http://cs.anu.edu.au/people/Ben.Lippmeier/">Ben Lippmeier</a>'s <a href="http://www.comp.mq.edu.au/~asloane/pmwiki.php/SAPLING/SAPLING071?action=download&upname=lippmeier-slides071.pdf">talk</a> at the <a href="http://www.comp.mq.edu.au/~asloane/pmwiki.php/SAPLING/SAPLING071">SAPLING June 2007 meeting</a> (<a href="http://www.comp.mq.edu.au/~asloane/pmwiki.php/SAPLING/SAPLING071?action=download&upname=lippmeier071.txt">talk summary</a>) explains region and effect inference for Haskell-like languages without sacrificing referential transparency or having to use the IO monad. This insight wouldn't solve the splay tree issue, because reading a splay tree <em>does</em> modify data that is not local to the reading function, though that modification should be opaque to clients.
</p>
<p>
I can't wait to see the full paper(s) and the implementation. Until I can, I'll have to settle for <a href="http://www.comp.mq.edu.au/~asloane/pmwiki.php/SAPLING/SAPLING061?action=download&upname=lippmeier061.pdf">the slides from an earlier talk with more motivation.</a>
</p>http://blog.jbapple.com/2007/06/proof-of-referential-transparency.htmlnoreply@blogger.com (Jim Apple)4tag:blogger.com,1999:blog-6839602.post-2752919249456839916Mon, 19 Mar 2007 01:00:00 +00002008-03-23T16:43:45.912-07:00constructive logiczero-knowledge proofExistentials and Zero-Knowledge Proofs<p>
When I use "∃ x . P(x)" in typed programming (using intuitionistic logic), I must have in hand an x and a proof of P(x). This is not the case in the classical logic, in which I might have a proof of ∃ x . P(x) without knowing any details of x at all.
</p>
<p>
This idea that I know such an x exists though I have no knowledge of it reminds me of <a href="http://en.wikipedia.org/wiki/Zero-knowledge_proof">zero-knowledge proofs</a>. Of course, the zero-knowledge proofs referenced in the Wikipedia article aren't so much proofs as they are assurances with high probability. I looked around for zero-knowledge proofs that were more proof-like, but I didn't find much. I wonder if there is any deeper connection between classical existentials and zero-knowledge proofs?
</p>http://blog.jbapple.com/2007/02/existentials-and-zero-knowledge-proofs.htmlnoreply@blogger.com (Jim Apple)1tag:blogger.com,1999:blog-6839602.post-4220869469690788347Mon, 19 Feb 2007 02:56:00 +00002008-03-23T16:46:43.246-07:00dependent typesGADTsHaskellMLSimulating Dependent Types with Guarded Algebraic DatatypesConor's Rule?<p>
<a href="http://www.dcs.st-and.ac.uk/~eb/">Edwin Brady</a> writes in <a href="http://edwinb.wordpress.com/2007/02/19/how-to-write-programs-in-two-easy-steps/trackback/">"How to write programs in two easy steps"</a>, that
<blockquote>
I think it's also an area where dependently typed languages like <a href="http://www.e-pig.org">Epigram</a> will shine, because it will one day be possible to write <a href="http://www.cs.st-andrews.ac.uk/~eb/writings/verified_staged.pdf"> <em>verified</em> interpreters</a> for domain specific languages …
</blockquote>
I immediately thought "I can <a href="http://www.cs.virginia.edu/~jba5b/singleton">write dependently typed programs <em>right now</em> with GADTs</a>, and I can do so in <a href="http://www.haskell.org/ghc/dist/current/docs/users_guide/data-type-extensions.html#gadt">GHC Haskell</a>, <a href="http://www.google.com/search?q=site%3Awww.scala-lang.org+gadts">Scala</a>, or the <a href="http://research.microsoft.com/~akenn/generics/index.html">upcoming C#</a>". This is, of course, only <em>mostly</em> true, since none of these does termination checking, and the syntax is awkward.
</p>
<p>
The same blog post later references <a href="http://en.wikipedia.org/wiki/Greenspun's_Tenth_Rule">Greenspun's Tenth Rule</a>:
<blockquote>
Any sufficiently complicated C or Fortran program contains an ad hoc, informally-specified, bug-ridden, slow implementation of half of Common Lisp
</blockquote>
and I thought that my programs follow a similar pattern with dependent types: I'm always simulating them informally. Based on Section 6.1: "The Trouble with Faking It" in <a href="http://www.cs.nott.ac.uk/~ctm/">Conor McBride</a>'s <a href="http://www.cs.nott.ac.uk/~ctm/faking.ps.gz">Faking It (Simulating Dependent Types in Haskell)</a> (<a href="http://citeseer.ist.psu.edu/mcbride01faking.html">mirror</a>), I wonder if there's any truth to something we might call
<dl>
<dt>Conor's Rule</dt>
<dd>Any sufficiently complicated Haskell or ML program contains an ad hoc, informally-specified, bug-ridden, half-completed simulation of dependent types.</dd>
</dl>
</p>http://blog.jbapple.com/2007/02/conors-rule.htmlnoreply@blogger.com (Jim Apple)1tag:blogger.com,1999:blog-6839602.post-2430773511442441263Sat, 10 Feb 2007 15:13:00 +00002008-03-23T16:40:47.496-07:00_|_continuityCPOsdefinabilityparallel orDefinability and Continuity<p>In <a href="http://japple.blogspot.com/2007/01/how-many-functions-are-there-of-type.html">How Many Functions are There of Type Bool -> Bool?</a>, I stated "The trick is to remember that if f is continuous, then f _|_ =/= _|_ implies that for all x, f x = f _|_". <strong>That is false</strong>. It would have been true had I said "… remember that if f is <ins>definable in Haskell</ins>, then …". The correct statement for continuous functions is: for all x, f x ≥ f _|_. The "≥" here is that used in domain theory to talk about <acronym title="Complete Partial Order">CPO</acronym>s.</p>
<p>In addition to only considering functions definable in Haskell, I was also only considering <dfn>flat</dfn> CPOs, in which each element is comparable only to itself and _|_. An example of a CPO that is not flat:
<pre>
data Wrap = Wrap Unit
data Unit = Unit
</pre></p>
<p>In the CPO Wrap<sub>_|_</sub>, _|_ < Wrap _|_ < Wrap Unit. Though Wrap<sub>_|_</sub> has three values, just like Bool<sub>_|_</sub>, there are only nine functions (continuous or definable in Haskell) of type Wrap<sub>_|_</sub> -> Bool<sub>_|_</sub>. Furthermore, there are eleven continuous functions of type Wrap<sub>_|_</sub> -> Wrap<sub>_|_</sub>, and all are definable in Haskell. (Thanks to Stefan O'Rear for pointing that out).</p>
<p>Clearly, the codomain isn't treated opaquely as it was in the last post: in order to count functions, we need to know the ordering on the codomain.
</p>
<p>
I have some more thinking to do about counting, continuity, and definability before I can make any more assertions about the cardinality of function types.</p>
<h6>Update:</h6>
<p>
Stefan O'Rear pointed out an error in which I claimed certain functions were not definable in Haskell, when they actually are. A better example of a function that is continuous but not definable in Haskell is:
<pre>
parallel_or _ True = True
parallel_or True _ = True
parallel_or False False = False
</pre>
</p>http://blog.jbapple.com/2007/02/definability-and-continuity.htmlnoreply@blogger.com (Jim Apple)0