tag:blogger.com,1999:blog-80724640599791741362024-03-12T17:33:00.490-07:00don't count on finding meheisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.comBlogger93125tag:blogger.com,1999:blog-8072464059979174136.post-25702700420560393392022-02-04T14:43:00.000-08:002022-02-04T14:43:06.377-08:00Pattern musings<h1 style="text-align: left;">A new breed of patterns</h1><p>I like to code up little snippets in Haskell to play around with interesting concepts. Sometimes I invent notation that must appear forcing to most, but let's introduce it anyway...</p><h2 style="text-align: left;">How I use <span style="font-family: courier;">ViewPatterns</span>, for fun and profit</h2><div>When writing evaluators, I like to use view patterns to evaluate subtrees already on the LHS (pattern side). Let's introduce a mini-language (also called Hutton's razor) that can only add:</div><div><br /></div><div><div><span style="font-family: courier;">data AST = Lit Integer | Plus AST AST deriving Show</span></div><div><br /></div><div>The evaluator is maximally simple, as it only needs to care about two sole cases:</div><div><br /></div><div><span style="font-family: courier;">eval :: AST -> Integer</span></div><div><span style="font-family: courier;">eval (Lit res) = res</span></div><div><span style="font-family: courier;">eval (Plus l r) = eval l + eval r</span></div><div><br /></div><div>There is a train of thought that cares about termination and logical consistency and thus requires that in the definition of <span style="font-family: courier;">eval (Plus l r)</span> the function to be defined can only be applied to structurally strictly smaller arguments (these are the <i>hypotheses</i>). We adhere to this rule above, but for more complicated functions it is possible to introduce bugs when not being super careful.</div><div>So why not resort to view patterns, and ban the <span style="font-family: courier;">eval</span> from the RHS altogether?</div><div><br /></div><div><span style="font-family: courier;">eval (Plus (eval -> l) (eval -> r)) = l + r</span></div><div><br /></div><div>This way of putting it makes it totally clear that <span style="font-family: courier;">eval</span> is always applied to parts of the syntax tree.</div><div><br /></div><h2 style="text-align: left;">Result patterns?</h2><div>But let's return to the base case (<span style="font-family: courier;">Lit</span>). We are forced to come up with a new binding (<span style="font-family: courier;">res</span>), just to have something in our hands that we can return? Sounds like redundancy. So for the purpose of this post I'll come up with a result pattern (=), which can appear on the LHS only once and it's presence there will rule out the RHS:</div><div><br /></div><div><span style="font-family: courier;">eval (Lit =)</span></div><div><br /></div><div>No more arbitrary names!</div><h2 style="text-align: left;">View lambdas, anyone?</h2><div>Okay, so let's turn up the heat a bit more. A <i>continuation-passing</i> interpreter is a tail recursive way to evaluate the AST:</div><div><br /></div><div><span style="font-family: courier;">cps :: forall k. AST -> (Integer -> k) -> k</span></div><div><span style="font-family: courier;">cps (Lit n) k = k n</span></div><div><span style="font-family: courier;">cps (Plus l r) k = cps l (\l -> cps r (\r -> k $ l + r))</span></div><div><br /></div><div>For the purpose of this exercise you can consider the type <span style="font-family: courier;">k</span> to be unit <span style="font-family: courier;">()</span>, and the continuation (value <span style="font-family: courier;">k</span>) a consumer of intermediate results. We recognise the same usage pattern as in <span style="font-family: courier;">eval</span>: subtrees are immediately (and linearly) passed to the function to be defined. So let's rewrite it with view patterns:</div><div><br /></div><div><span style="font-family: courier;">cps (Plus (cps -> l) (cps -> r)) k = l (\l -> r (\r -> k $ l + r))</span></div><div><br /></div><div>But now we face the same redundancy issue, that the view patterns bind identifiers that are somehow repetitive, as they are applied to lambdas immediately. Can we come up with a notation for a view pattern that applies on a lambda and extends its scope to the rest of the patterns and to the RHS? Consider</div><div><br /></div><div><span style="font-family: courier;">cps (Plus (cps -> \l) (cps -> \r)) k = k (l + r)</span></div><div><br /></div></div><div>It takes some time to see the charm here, as it is wormholing a lambda-bound identifier to the RHS, but it is unbeatably concise. And we can combine it with the result pattern idea too:</div><div><br /></div><div><span style="font-family: courier;">cps (Plus (cps -> \l) (cps -> \r)) (($ l + r) -> =)</span></div><div><br /></div><div>At this point however the readability is suffering.</div><h2 style="text-align: left;">Outro</h2><div>Note that the view lambdas are strange beasts, not only because they wrap the result (RHS or <span style="font-family: courier;">=</span> pattern), but also the identity holds: <span style="font-family: courier;">\p</span> ≡ <span style="font-family: courier;">(id -> \p)</span>, but since all the ids don't change anything, they can be stripped anyway. I wonder where I shall encounter more such view lambdas in the wild...</div>heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-38841698802328327032014-11-06T15:57:00.001-08:002014-11-06T15:57:31.333-08:00Unembedded associationsEverytime I start understanding the gist of a paper that appeared unfathomable to me a few months before, a strange thing happens to me. My brain often wanders off, and creates interesting new bridges, on which my thoughts begin to run and reach new previously unchartered land. This same thing happened to me when reading Atkey et al.'s <a href="http://bentnib.org/unembedding.html">"Unembedding Domain-Specific Languages"</a>. Here I encountered my old friend, the HOAS lambda vocabulary <br />
<code><br />
class LC expr where<br />
lam :: (expr → expr) → expr<br />
app :: expr → expr → expr<br />
</code><br />
<br />
Freely associating I came up with an idea how to simulate a limited form of duck typing for conditionals:<br />
<code><br />
class Condition expr<br />
toBool :: expr → Bool<br />
cond :: expr → a → a → a<br />
cond c th el = if toBool c then th else el<br />
</code><br />
<br />
This would allow to retrofit many condition-like data types with this vocabulary. <code>Nothing</code>, <code>0</code>, <code>(Left _)</code> all could serve as <i>false</i>.<br />
<br />
Maybe I could even follow Conor McBride's advice and make the then and else arms of the conditional differently typed. Though I would need associated types for that.<br />
<br />
Duck typing may turn out like a good idea in a statically typed language, when implemented this way. Another use case would be function application by the built-in juxtaposition syntax. It already means different things in different syntactic contexts, like function application or type (family) application. <a href="https://personal.cis.strath.ac.uk/conor.mcbride/pub/she/idiom.html" target="_blank">Idiom brackets</a> come to my mind. Edward Kmett's <code><a href="http://hackage.haskell.org/package/semigroupoids-4.2/docs/Data-Functor-Bind.html#t:Apply" target="_blank">Apply</a></code> class looks like a good candidate for a related vocabulary. The typing rule would be implemented by an associated (injective) type family. Hopefully someday we'll see <code>-XRebindableSyntax</code> for value-level application, that is type-directed.heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-70366059554237200472014-10-26T16:09:00.000-07:002014-10-26T16:44:14.262-07:00gdiff – PolymorphicallyIn the few last months I've been busy coming up with techniques mastering the <a href="https://hackage.haskell.org/package/gdiff" target="_blank"><code>gdiff</code> Haskell library</a>, even for use cases it was not originally designed for.<br />
This is mostly a brain dump of some approaches I have learnt while tinkering and trying to solve certain problems.
<br />
<br />
1) Polymorphic <code>diff</code>: Eelco Lempsink writes in the conclusion of his <a href="http://eelco.lempsink.nl/thesis.pdf" target="_blank">2010 thesis</a> «Furthermore, we can not encode polymorphic datatypes such as lists, but need to write specific encodings for each type we want to include». In the <a href="https://hackage.haskell.org/package/gdiff-1.1/docs/Data-Generic-Diff.html#g:5" target="_blank">library documentation</a> he says «It might require another master thesis project to solve this». However in the last days I developed a trick, which does allow me to describe polymorphic data types, such as <code>[a]</code> or <code>Maybe a</code>. I just needed to add these lines:<br />
<br />
in the family GADT:<br />
<code>
ListNil :: List Fam as → Fam a as → Fam [a] Nil<br /> ListCons :: List Fam as → Fam a as → Fam [a] (a `Cons` [a] `Cons` Nil)<br /><br />
</code>
then define a <code>Type</code> instance:<br />
<code>
instance Type Fam a ⇒ Type Fam [a] where<br />
constructors = head [Concr (ListNil cc) | Concr cc Concr cc ← constructors] : [head [Concr (ListCons cc) | Concr cc ← constructors]]</code><br />
<br />
What is this doing? It picks two random constructors from the underlying data type and wraps them with <code>ListNil</code> and <code>ListCons</code>. We usually ignore what is wrapped, with one exception: in <code>decEq</code> one needs to ensure that the constructors' arguments are compared too, otherwise one cannot finish the type equality proof.<br />
<br />
2) Non-moving pairs: In the usual textual <code>diff</code> algorithm the lines may move around a bit to make room for insertions, etc. This is normally the case for <code>gdiff</code> too. I have seen <code>gdiff</code> reusing values (with <code>Cpy</code>) when comparing <code>(True, False)</code> with <code>(False, True)</code>. But sometimes this is not desired at all. I figured out that "inlining" the leaves into the pair's description (i.e. instead of <code>(a `Cons` b `Cons` Nil)</code> writing <code>appendList</code> on the field decompositions of <code>a</code> and <code>b</code> does the trick.<br />
<br />
3) Location types: I found a way to equip <code>Abstr</code> constructor descriptors with type class dictionaries. It is similar to the lifting approach shown under 1), but much more involved.<br />
The idea is to wrap a location-aware descriptor with a descriptor that is location-blind, i.e. that hides the location parameter:
<code>Loc' :: KnownNat n ⇒ Fam (Loc n Bool) …</code>
<br />
Then we need the wrapper:<br />
<code>Hidden' :: KnownNat n ⇒ Fam (Loc n Bool) ts → Fam (Hidden Loc) ts</code>
<br />
Giving the <code>Type</code> instance for the latter is tricky, as <code>Abstr</code> alone has no provision for dodging the class dictionary into <code>Hidden'</code>, so I had to write a <code>locAware</code> smart constructor to syphon it through the <code>Hidden'</code> wrapper.<br />
This also stressed the compiler to its limits in the advanced <code>PolyKind</code>-ed approach I needed, so I filed a <a href="https://ghc.haskell.org/trac/ghc/ticket/9725" target="_blank">GHC bug #9725</a>. There is also some code showing how the <code>Hidden Loc</code> is unwrapped and the dictionary-passing functions is installed into the <code>Abstr</code>.
<br />
<br />
4) Monadic actions coming out of <code>patch</code>: Here another wrapping approach is needed, but this time we need a sum type for <code>diff</code> and <code>patch</code> so that we can enter with a pure value at the <code>Left</code> and obtain a <code>Right</code> action back. This is the most involved approach. I can probably blog another time about it.heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-91016538147683764922014-08-07T01:27:00.000-07:002014-08-07T01:27:19.023-07:00First Programming with my DaughterToday I had a short programming session with my 7 year old. I had shown her earlier what a list is and she came back several times already to show her "more lists".<br />
So this time I thought we could do something more interesting. A letter-changing game! I fired up GHCi and entered:<br />
<br />
<code>
Prelude⟩ let satz = "Leleka hat Kacke in der Hose"<br />
Prelude⟩ print satz<br />
"Leleka hat Kacke in der Hose"<br />
</code>
<br />
<br />
She loved it so far. Fun is the strongest motivator to learn for kids…<br />
<br />
Then came the changer for letters:<br />
<br />
<code>
Prelude⟩ let tausch = \x → case x of {'L' → 'K'; 'e' → 'i'; 'i' → 'u'; 'u' → 'e'; x → x }<br />
</code><br />
<br />
Then I applied it on the phrase defined earlier:<br />
<br />
<code>
Prelude⟩ map tausch satz<br />
"Kilika hat Kacki un dir Hosi"<br />
</code><br />
<br />
This did it. She kept repeating the transformed sentence for an hour, giggling. I tried to explain to her what we did just now, but I guess I'll wait till next time to make her repeat this exercise.heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-80390455990711700042014-07-31T14:28:00.000-07:002014-07-31T14:45:28.905-07:00Rank-2 PHOASLately I've been experimenting with <i>finally-tagless</i> (typed) representations and made an attempt to model the (implicitly typed) lambda calculus. However, I wanted to use the <i>parametric higher-order abstract syntax</i> (PHOAS) technique to obtain variable bindings that are automatically well-scoped.<br />
I arrived at this formulation:<br />
<br />
<code>
class LC rep where<br />
var :: p → rep<br />
lam :: (forall p . p → rep) → rep<br />
</code><br />
<br />
(I am ignoring applications as they are not important for making my point.)<br />
As Andres Löh has pointed out to me this is not the final-tagless formulation of the regular PHOAS form, as that would add the <code>p</code> type variable as the second class parameter and the rank-2 <code>forall</code> would appear from "outside".<br />
But I liked my simple formulation and the obviously and explicitly parametric lambda body. So I started implementing a rudimentary visualisation instance given a name supply:<br />
<br />
<code>
instance LC ([String] → String) where<br />
var = ??? -- const "VAR"<br />
lam f = \supply → ...<br />
</code><br />
<br />
It turns out that implementing <code>var</code> is only possible by giving a constant result, and for <code>lam</code> I am in trouble, because I cannot call <code>f</code> as it expects a polymorphic argument. Both problems are due to the fact that <code>p</code> is too polymorphic. Can we have it a bit less polymorphic in order to make some progress?<br />
Thinking about it I came up with the idea of giving each instance a way to constrain the <code>p</code> variable as it fits. So I changed <code>class LC</code> such:<br />
<br />
<code>
class LC rep where<br />
type Restricted rep p :: Constraint<br />
var :: Restricted rep p ⇒ p → rep<br />
lam :: (forall p . Restricted rep p ⇒ p → rep) → rep<br />
</code><br />
<br />
Now my instance can pick the restriction as it fits:<br />
<br />
<code>
instance LC ([String] → String) where<br />
type Restricted ([String] → String) p = ([String] → String) ~ p<br />
var = id<br />
lam f = \supply → ...<br />
</code><br />
<br />
As you see I chose the restriction to be <i>type equality</i> which essentially cancels parametricity in this instance and gives me simple HOAS. Filling in <code>p</code> becomes easy now.<br />
<br />
<code>
lam f = \(n:ns) → "\\" ++ n ++ "." ++ (f $ const n) ns
</code><br />
<br />
Let's try it out! But in order to do that we need an instance of <code>Show</code> for name supplies. This could be one:
<br />
<code><br />
instance Show ([String] → String) where<br />
show f = f $ map (('v':) . show) [0..]<br />
</code><br />
<br />
Now we can interpret a lambda term as a name supply.
<br />
<code><br />
*Main› lam (\x → lam $ \y → var x) :: [String] → String<br />
\v0.\v1.v0
</code><br />
<br />
It works™ :-)<br />
<br />
But I can go further. After implementing several other instances I observed that I always wanted to destroy parametricity completely and implement <code>var</code> as the identity. So why not have these as defaults and reduce the boilerplate by a nice margin? Here is the final class definition that I arrived at:<br />
<br />
<code>
class LC rep where<br />
type Restricted rep p :: Constraint<br />
type Restricted rep p = rep ~ p<br />
var :: Restricted rep p ⇒ p → rep<br />
default var :: rep ~ p ⇒ p → rep<br />
var = id<br />
lam :: (forall p . Restricted rep p ⇒ p → rep) → rep<br />
</code><br />
<br />
I like it so far.<br />
<br />
PS: Here are the prerequisites if you want to compile the above yourself:<br />
<code><br />
{-# LANGUAGE UnicodeSyntax, ConstraintKinds, TypeFamilies, RankNTypes, FlexibleInstances, DefaultSignatures #-}<br />
<br />
import GHC.Exts<br />
</code>
heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-20953917458015142452014-01-12T18:45:00.001-08:002014-01-15T02:42:00.526-08:00Testing LaTeX with MathJax<script src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script>
<script type="text/x-mathjax-config">
MathJax.Hub.Config({
tex2jax: {
inlineMath: [ ['$','$'] ],
displayMath: [ ['$$','$$'] ],
processEscapes: true
}
});
</script>
$3_{5}$
$$42^{25}$$
<br />
extensions: ["tex2jax.js"],
jax: ["input/TeX", "output/HTML-CSS"],
<br />
Does <strike>not</strike> work<br />
<br />
But this:
<br />
<blockquote class="tr_bq">
<script src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script></blockquote>
<blockquote class="tr_bq">
<script type='math/tex; mode=display'>
\{ 0, 1, 2 \}
</script>
</blockquote>
Results in something pretty:
<script type="math/tex; mode=display">
\{ 0, 1, 2 \}
\mathcal{L}
</script>
heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-38894734103355238352013-09-02T01:26:00.002-07:002013-09-02T01:42:49.841-07:00Now it's evident — totally!In <a href="http://heisenbug.blogspot.de/2012/12/decidable-equality.html" target="_blank">one of my posts</a> about logics I have shown that a proof of a true proposition consists of constructing a function from ⊤ (truth) to an inhabitant of that proposition (interpreted as a type).<br />
<br />
Dually, one would hope, we must construct a function between false propositions and ⊥ (bottom, the empty set).<br />
<br />
The big question is: <i>How?</i> There appear to be many functions into the empty set. These surely cannot mean to be proofs!<br />
<br />
There is a catch: <i>totality</i>. For every possible input we are obliged to provide a well-defined, deterministic result. A hard job when the target set is empty!<br />
<br />
On the other hand it is easy enough for positive proofs: (considering the finite case...) say, we seek a proof of the <code>Bool</code> proposition. <code>Bool</code> has two inhabitants, so the function space from ⊤ (single inhabitant) to <code>Bool</code> must have 2<sup>1</sup> of them. Here is one:<br />
<br />
<code>provebool () = True</code><br />
<br />
(Do you find the other one?)<br />
<br />
But for negative proofs, it isn't really obvious how to do it. Since refutable propositions (allegedly) have no inhabitants, how do we write a pattern-matching function between them?<br />
<br />
But remember, in the finite proof case our arrows had n<sup>m</sup> inhabitants, picking any one of these constituted a valid proof.<br />
<br />
For the uninhabited case such a way of counting gives us a clue: 0<sup>0</sup> can be interpreted as 1! And this is the key, we need to do pattern matching with <i>no patterns</i> to get that inhabitant:<br />
<br />
<code>refutation = \case of {}</code><br />
<br />
When this function is total, we have our sought-for unique proof. And for actual negative proofs it evidently is! heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-4158376066577736812013-08-20T13:03:00.000-07:002013-08-31T14:57:17.485-07:00VerschiedenesMein Vater wäre morgen 72 geworden. Ich habe mich schon lange daran gewöhnt, daß er nicht da ist, dennoch habe ich ruhige Momente, wo ich mir wünschte ich könnte ihm erzählen was ich so mache.<br />
<br />
Er würde es verstehen.<br />
<br />
Er sagte mir einmal "Ich hätte es geschafft dich in die Medizin zu bugsieren, wenn ich dort eine Zukunft gesehen hätte." Ich glaube er sah im ganzen medizinischen Komplex keine Zukunft, mit Sicherheit auch im finanziellen Aspekt. Oder er sah einfach keine Perspektive darin, für <i>mich</i>. Auf alle Fälle stand er meinen mathematischen Ambitionen sehr aufgeschlossen gegenüber. Er kaufte mir das Buch das ich immer noch sehr verehre, "A fizika kultúrtörténete" (die Kulturgeschichte der Physik). Ich habe es vor kurzem meinem Sohn auf englisch gekauft.<br />
<br />
Das aus meinen Ambitionen nicht wirklich viel wurde, lag wahrscheinlich daran, daß ich in die Informatik gegangen bin ;-)<br />
<br />
Aber egal, es macht mir ja viel Spaß, und die beiden Gebiete verzahnen sich ja zusehends. Es gibt einen signifikanten Trend, die Grundlagen der Mathematik auf das Fundament der Typentheorie zu stellen, und somit die Mengenlehre praktisch zu entthrohnen, nach mehr als 100 Jahren Herrschaft.<br />
<br />
In einem kleinen Winkel dieses Kriegsschauplatzes mache ich mir selber gedanken. Gestern Abend fuhr ich nach Ansbach, um meine Mutter zu besuchen, und nahm auch Hamster Daniela mit. Ich war wirklich müde geworden nach dem Abendessen, las noch ein Paar Seiten Kategorientheorie und schlief ein. Aber zwischen 2 und 3 wachte ich auf, und ich denke in dem Moment verstand ich, daß meine Idee von Typen als Flächen sich mit den Opetopen vereinbaren lassen, wenn man sich nur in die Kodimension versetzt. Das Stichwort Poincaré-Dualität kommt da auf, was alles erklären könnte.<br />
Ich nahm den Hamster mit runter, wir setzten uns vor die Terrassentür, und der Schein des Vollmondes fiel auf uns. Es war mystisch.<br />
<br />
Außerdem arbeite ich an einer Kodierung, so daß etwas gleichwertiges zum Lambda-Kalkül mit Opetopen kodiert werden kann. Mal schauen wie das alles zusammenkommt.<br />
<br />
Ich denke mein Vater wäre der einzige aus meinem Umkreis der für solche Gedanken ein wirklich offenes Ohr gehabt hätte, selbst wenn er das meiste gar nicht verstanden hätte. Aber er wäre auf mich manchmal stolz gewesen.heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-82911147188901536232013-08-19T07:49:00.000-07:002013-09-02T00:43:13.207-07:00Compiling GHC on RHEL6Compared to building GHC on RHEL5 this is a breeze.<br />
<br />
<code>git</code> is in the installation — <span style="color: #6aa84f;">check</span><br />
<code>perl boot</code> — <span style="color: #6aa84f;">check</span><br />
<code>./configure</code> — <span style="color: #e69138;">breaks</span>, linker does not find <code>libgmp.so</code><br />
I built <code>gmp</code> from sources, and installed it into my home directory.<br />
<br />
But... it still did not build :-(<br />
<br />
As always, <a href="http://stackoverflow.com/questions/13292261/ld-library-path-doesnt-seem-to-work">Stack Overflow</a> for the win!<br />
<br />
Specifying<br />
<code>setenv LIBRARY_PATH $HOME/lib</code><br />
did the trick.<br />
<br />
For good measure I also added<br />
<code>--with-gmp-libraries=</code><code><code>$HOME/lib</code> --with-gmp-includes=</code><code><code>$HOME</code>/include</code><br />
to the configure line, but this might be redundant?<br />
<br />
(Another thought, find seems to reveal some <code>libgmp.so</code> under <code>/usr</code>, I might point it there.)<br />
<br />
So, finally, <br />
<span style="color: #6aa84f;"></span><br />
<code>./configure ...</code> — <span style="color: #6aa84f;">check</span><br />
<br />
The part that involves building was the pleasure part:<br />
<br />
<code>nice make -j14</code> — <span style="color: #6aa84f;">check</span><br />
<br />
Then I dared running the test suite:<br />
<br />
<code>make test</code> — <span style="color: #6aa84f;">check</span><br />
<br />
This step takes its time, as it is not parallelizable. <br />
<br />
There is only one drop of bitterness, namely the <code>stage2</code> compiler does not run on RHEL5. But that is something I did not expect, actually.<br />
<br />
<code>make install</code> — <span style="color: #6aa84f;">check</span><br />
<br />
nothing unexpected here.<br />
<br />
Have fun with GHC on RHEL6!heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-32139297439408181712013-08-10T05:11:00.001-07:002013-08-10T05:54:59.863-07:00Proudly presenting the »nopetope«!(This is is jotted down, raw posting, that may never get finished. I am publishing it anyway, as it pretty much reflects my current mood.)<br />
<br />
I am about to do some research with coverings of trees, and it was only natural to look at Baez-Dolan metatrees and the corresponding notion of opetopes.
<a href="http://arxiv.org/pdf/0706.1033.pdf" target="_blank">The paper</a> contains a famous 5-minute definition and it is a brain teaser worth reading. They introduce trees and nestings (actually two sides of the same coin) and their superposition, called a constellation, which has to follow some rules, but drawing spheres is a creative process.<br />
<br />
Then there are zooms which connect constellations as long as the left nesting and the right tree are morally identical.<br />
<br />
My lambda graphs are basically search trees and a nesting would add the operational notion of evaluation.
Since we can freely choose our evaluation strategy (confluence?), the latter corresponds to a nesting.
It remains to find out what the degenerate zooms are under this aspect.<br />
<br />
I am just reading the "Polynomial functors and opetopes" paper (http://arxiv.org/pdf/0706.1033.pdf) and it asserts that it's starting constellation is a one leafed tree:
<pretty here="" picture="">
But I wonder if this is fundamental, and since leaves are stripped by zooms, any number will do.</pretty><br />
<pretty here="" picture="">So I'll suggest starting with zero leaves, and calling the resulting zoom complex(es) the nopetopes. This might be the first mathematical term I have coined :-)</pretty><br />
<br />
<pretty here="" picture="">For the mathematically-challenged, a nopetope is just a lollipop wrapped in cellophane, while an opetope is the two-stick version thereof.</pretty><br />
<br />
<pretty here="" picture="">It is a funny coincidence that "one" and "ope-" contain the same vocals. Going on, we could also have twopetopes and thropetopes, fouretopes etc. But I doubt these are significant in any way.</pretty><br />
<br />
<pretty here="" picture="">And now back to the paper and then to an <a href="http://code.google.com/p/omega/">Ωmega</a> implementation of nopetopes...</pretty><br />
<br />
<pretty here="" picture="">PS: while writing this my imagination went though... Are trees and nestings compatible with the famous correspondences
energy-mass, wave-particle of physics? Looks like I have to start some more research.</pretty>heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-46577730957211343712013-02-27T11:40:00.002-08:002013-02-27T11:46:28.035-08:00Old Cabal SubhellSometimes I have a cabal that is too old for generating up-to-date boilerplate files for package installs, so I have to install a new <code>cabal-install</code>. But unfortunately I run into the same problem when installing the HTTP package, which is needed for cabal itself. So I am in a (pun totally intended, as you'll see later on) <a href="http://en.wikipedia.org/wiki/Catch-22">catch-22</a>, and each time I feel being lost completely.<br />
<br />
But there is a cure to this particular problem:<br />
<br />
create a modified<br />
<br />
<code>mv dist/build/autogen/Paths_HTTP.hs dist/build</code><br />
<br />
and patch it with<br />
<br />
<code>
$ diff -u dist/build/autogen/Paths_HTTP.hs dist/build<br />
--- dist/build/autogen/Paths_HTTP.hs 2013-02-27 20:07:01.437225000 +0100<br />
+++ dist/build/Paths_HTTP.hs 2013-02-27 20:20:36.735526000 +0100<br />
@@ -6,6 +6,7 @@<br />
<br />
import Data.Version (Version(..))<br />
import System.Environment (getEnv)<br />
+import Control.Exception<br />
<br />
version :: Version<br />
version = Version {versionBranch = [4000,2,8], versionTags = []}<br />
@@ -17,11 +18,14 @@<br />
datadir = "/home/ggreif/share/HTTP-4000.2.8"<br />
libexecdir = "/home/ggreif/libexec"<br />
<br />
+hardCoded :: FilePath -> IOException -> IO FilePath<br />
+hardCoded dir = const $ return dir<br />
+<br />
getBinDir, getLibDir, getDataDir, getLibexecDir :: IO FilePath<br />
-getBinDir = catch (getEnv "HTTP_bindir") (\_ -> return bindir)<br />
-getLibDir = catch (getEnv "HTTP_libdir") (\_ -> return libdir)<br />
-getDataDir = catch (getEnv "HTTP_datadir") (\_ -> return datadir)<br />
-getLibexecDir = catch (getEnv "HTTP_libexecdir") (\_ -> return libexecdir)<br />
+getBinDir = catch (getEnv "HTTP_bindir") (hardCoded bindir)<br />
+getLibDir = catch (getEnv "HTTP_libdir") (hardCoded libdir)<br />
+getDataDir = catch (getEnv "HTTP_datadir") (hardCoded datadir)<br />
+getLibexecDir = catch (getEnv "HTTP_libexecdir") (hardCoded libexecdir)<br />
<br />
getDataFileName :: FilePath -> IO FilePath<br />
getDataFileName name = do<br />
</code>
<br />
<br />
This file is then preferably found by GHC and all is okay. Incidentally I already employed this trick in the past, but forgot about the details so I had to reinvent it again.<br />
<br />
After escaping this particular subhell of cabal I came up with this blog post in order to not lose my way in the future. Hopefully it helps you too.heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-43452587695748095962012-12-19T07:21:00.002-08:002013-09-02T01:42:21.217-07:00Decidable equalityTrailing <a href="http://typesandkinds.wordpress.com/2012/12/01/decidable-propositional-equality-in-haskell/">Richard Eisenberg's blog post</a> I've been triggered to recollect what I have read about the matter so far. Turns out that I was about 17 when I first came into contact with the concept. After my brother hinted to me a month ago that he is reading <a href="http://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach">"Gödel, Escher, Bach"</a>, I grabbed my own copy from my bookshelf and quickly found the page about the fractal nature of provable propositions and the true-false divide. I have scanned it and showing it below.<br />
<br />
<div class="separator" style="clear: both; text-align: center;">
<a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEicMr_ugBx2jd0Jjl_hIGEWKF8S8fLQg5bUm3ZMLmkXyP7Rpe_axqr4pqWorGv0diT0UH4AEtk4TiHGX_KofwWZp1qlPEHEFUIcTXLUeDfYnTFWZ4FqIbJFVYmuLezsZUj2BtMiJ69T6Ow/s1600/GEB-Proofs.png" imageanchor="1" style="margin-left: 1em; margin-right: 1em;"><img border="0" height="320" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEicMr_ugBx2jd0Jjl_hIGEWKF8S8fLQg5bUm3ZMLmkXyP7Rpe_axqr4pqWorGv0diT0UH4AEtk4TiHGX_KofwWZp1qlPEHEFUIcTXLUeDfYnTFWZ4FqIbJFVYmuLezsZUj2BtMiJ69T6Ow/s320/GEB-Proofs.png" width="244" /></a></div>
<br />
What is the connection to decidable equality? I believe this illustration shows it:<br />
<br />
<div class="separator" style="clear: both; text-align: center;">
<a href="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgKofSOXNw78M52GcnWOB7iU7f2u5hCtp4uF6DoXte1IbAanM0gLGZ4pKJy5JNk6Aa9tELlZbSuVCqAJG-1XAuewV__yQFNktPjeA7Rjzb7mfPelj0kpWiD6IVpcN9ZZ7oLjhZsvIGPxcM/s1600/DecidableEquality.png" imageanchor="1" style="clear: left; float: left; margin-bottom: 1em; margin-right: 1em;"><img border="0" height="312" src="https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgKofSOXNw78M52GcnWOB7iU7f2u5hCtp4uF6DoXte1IbAanM0gLGZ4pKJy5JNk6Aa9tELlZbSuVCqAJG-1XAuewV__yQFNktPjeA7Rjzb7mfPelj0kpWiD6IVpcN9ZZ7oLjhZsvIGPxcM/s320/DecidableEquality.png" width="320" /></a></div>
I have depicted <span style="font-family: "Courier New",Courier,monospace;">T</span> (truth, top, any nullary constructor, e.g. <span style="font-family: "Courier New",Courier,monospace;">()</span>) at the north pole, and bottom (false, ⊥) at the south pole. The way or reasoning on the north hemisphere is to <i>transport truth into a type</i>, i.e. construct a function of type <span style="font-family: "Courier New",Courier,monospace;">()<span class="st">→</span>P</span>, where <span style="font-family: "Courier New",Courier,monospace;">P</span> is the proposition we want to prove in Curry-Howard encoding. As the figure shows we may have a finite number of stops on our way. We can note that a function of type <span style="font-family: "Courier New",Courier,monospace;">()<span class="st">→</span>P</span> is isomorphic to <span style="font-family: "Courier New",Courier,monospace;">P</span>, so simply constructing an object of type <span style="font-family: "Courier New",Courier,monospace;">P</span> suffices.<br />
<br />
Dually, proving that a proposition is false, we have to construct a path to bottom from <span style="font-family: "Courier New",Courier,monospace;">Q</span>, again possibly via a finite number of stops. Since (<span style="font-family: "Courier New",Courier,monospace;">Q<span class="st">→</span>⊥</span>) cannot be simplified we really have to construct functions here.<br />
<br />
The equator divides true from false and thus separates the duals.<br />
<br />
Since each proof (when computable in finite time) will either result in something from the blue or red island, the type for decidable equality must be <span style="font-family: "Courier New",Courier,monospace;">Either (a :~: b) ((a :~: b) -> Void)</span>.heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com1tag:blogger.com,1999:blog-8072464059979174136.post-74455554666583610282012-09-18T14:29:00.000-07:002012-09-18T14:30:44.078-07:00Thrist sightingsIt's been a bit quiet recently, but not inactive. Edward Kmett has adopted the <a href="https://github.com/ekmett/indexed/blob/master/src/Indexed/Thrist.hs#L22">name and the concept</a> in two of <a href="https://github.com/ekmett/multipass/blob/master/Data/Pass/Thrist.hs#L24">his libraries</a>. Of course the concept is much older than the name, being a path in some category.<br />
<br />
If you look carefully, in the middle of his ICFP '12 keynote Conor McBride derives thrists (he keeps the name <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">List</span> in his development) and they may also appear in the <a href="https://personal.cis.strath.ac.uk/conor.mcbride/Kleisli.pdf">JFP article</a> where they are named <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">Path</span>.<br />
<br />
Only with the advent of GADTs and user defined kinds in systems like Ωmega, SHE and Agda the concept of threading types begins to blossom. Since the release of GHC v7.6.1 the most popular Haskell compiler also supports kind polymorphism. This prompted me to re-spin the <a href="http://hackage.haskell.org/package/thrist">thrist package</a> to take advantage of GHC's new feature.<br />
<br />
Have fun,<br />
<br />
Gaborheisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-69562966966776315682011-12-26T17:11:00.000-08:002011-12-26T17:11:57.062-08:00Showing Thrists RevisitedMore than three years ago I <a href="http://heisenbug.blogspot.com/2008/08/id-like-to-see-but-do-you-want-to-show.html">lamented</a> that it's impossible to to define a <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">show</span></span> function on thrists, generally, even when the element type is member of the <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">Show</span></span> class.<br />
<br />
In the meantime I succeeded to declare <a href="http://svn.berlios.de/svnroot/repos/al4nin/trunk/purgatory/Appli.hs?p=1129">certain thrist parametrizations</a> and convince GHC to accept show instances for them. The <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">Appli</span></span> thrist is such an example.<br />
<br />
With the <a href="http://www.haskell.org/pipermail/glasgow-haskell-users/2011-December/021310.html">upcoming GHC 7.4</a> things may improve considerably, as it will bring <i>constraint kinds</i>. Remember, thrists are (currently) parameterized like this <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">(* → * → *) → * → * → *</span></span>, i.e. on <i>types</i>, and with the new <i>kind variable</i> feature we can probably generalize to <i>user-defined kinds</i>. Then the parameters may match Ωmega's: <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">(a → a → *) → a → a → *</span></span>. So we still result in a type, but we can choose our indices from a vastly bigger domain. Enter constraint kinds! These may be part of our user-defined kinds, so we can form stuff like <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">(Show, *)</span></span> and supply it for the parameter <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">a</span></span>. With some luck deriving <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">Show</span></span> can be more successful and not attached to particular parametrizations.<br />
<br />
I regrettably still haven't gotten around building a GHC v7.4.1 candidate, so I cannot verify the above, but my gut feeling is that this'll work out...heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com1tag:blogger.com,1999:blog-8072464059979174136.post-29874043627874761772011-11-22T15:03:00.000-08:002011-11-22T15:03:38.059-08:00Pondering about the FoundationsAs I am thinking about how a possible Ω<i>mega 2.0</i> could be implemented, I am trying to come up with some interesting concepts w.r.t. parsing and type checking. Since no single line is written yet, it is easy and cheap to ponder.<br />
<br />
Some key elements are already taking shape in my mind. These are:<br />
<ul><li>parsed entities carry their start and end coordinates in their types</li>
<li>there is no difference between patterns and expressions</li>
<li>each expression carries a typing thrist.</li>
</ul>The second item has been elaborated by me in an earlier post. The third must wait a bit until I have something coherent (but the curious reader might visit my <a href="http://code.google.com/p/omega/wiki/HomologyTypes">sketch of ideas</a>).<br />
<br />
I'd like to talk about item one here. The essence is that every grammar element obtains a type that describes where this element is located. For example a function declaration may occupy the text portion between <i>start</i> and <i>end</i>, where these are type-level triples (file, line, column). In order to consider parsed input consistent, the start coordinates must be aligned with the prior element's end coordinates, i.e. we have another thrist here.<br />
<br />
Things get interesting when we model naming and scope. Name definition and referral must somehow match the types, after the match is done the semantics can be read off the user. To give an example:<br />
<blockquote class="tr_bq"><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">Ref definer :: Exp (`foo, 42, 7) (`foo, 42, 11)<br />
where definer :: Exp (`foo, 41, 1) (`foo, 45, 37) = ...</span></span></blockquote>Both the reference and the definition live in the same file "foo.prg". The former is on line 42 from column 7 to 11 (exclusive). The definition it refers to is in fact enclosing it (a recursive call, maybe?) extending from line 42 to 45. With this representation the name of the indentifier becomes secondary, all that counts is the evidence in <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">definer</span></span> which contributes to its type! We have created a <i>globally nameless</i> representation.<br />
<br />
We can expand this world view to also include the level of the grammatical entity (value, type, kind, etc.) as a fourth coordinate. So a reference to a ›25‹ somewhere in the text at floor 0 would point to an integer literal, the same place at floor 1 to the type <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">Int</span></span> and at floor 2 it would be the kind <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">*</span></span>.<br />
<br />
My hope is that all the proof obligations arising in such a scheme can be cleverly extracted from a parsec-like engine.heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-2850978433674820202011-10-05T21:39:00.000-07:002011-10-06T06:07:22.856-07:00Macs and meI am profoundly saddened since I woke up at 4:00am in the morning, and saw the news headline about the passing of Steve Jobs. I have seen this coming for a long time, as my father died in a very similar way back 1993 with only 52. Looking at the thin appearance of Jobs in the last month or even years I constantly get reminded of him. Basically the same story of suffering, loss of weight, liver transplant (in vain), death. RIP, Dad, RIP, Steve.<br />
<br />
I am writing this on a rusty vintage 2000 PowerBook G4 Titanium, I bought on eBay last year, because the video of my own 2001 TiBook went black. By today's web standards completely inadequate, it serves me well for news reading, terminal logins, etc. My son Pedro got his MacBook Pro 15'' delivered just today. An awesome piece of technology.<br />
<br />
My father bought the first Mac in 1986, just after opening his practice as a neurologist. This was two years after cutting all strings in Hungary and fleeing to Germany in a pretty bold move. Must have been a moment of total self-overestimation when I promised to my dad "if you buy that Mac Plus I'll write you the best software for it for your doctor's office". A crazy time began. At day the Mac was used to keep patient's data with a DTP program "RagTime", at 5pm I hauled the Mac home (in a big black bag) and started writing the program. Sometimes deep into the night. I used Turbo Pascal (and later MPW) after figuring out that the Lisp environment I preferred simply did not cut it due to insufficient support of the Toolbox. In the morning my father carried the Mac back and powered it up.<br />
<br />
Less than year later the program was ready for productive work. A Mac SE joined the party and we had a networked doctor's application with a really neat windowed user interface, that would put even today's programs to shame in this regard.<br />
<br />
There was even a time when we fancied marketing this product, but my university duties and the early death of my father simply negated all plans to this end.<br />
<br />
When I had my diploma in my hands I picked up the phone and called the guy who sold us the Mac Plus and a copy of "Inside Macintosh" back in '86. In the meantime he founded a pretty successful company around a networked admin solution called 'netOctopus' which was his baby. We occasionally met at Apple developer events and I new that he was a pretty damn good coder. He hired me and I was earning money by programming Macs!<br />
<br />
So yes, I love Macs and there is no reason that this will change in the foreseeable future.<br />
<br />
I kept telling to myself, should Jobs die one day, I'll put that Mac Plus (now in my basement and still functional) up for sale at eBay. My thought today: "screw it – too many fond memories attached".heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com3tag:blogger.com,1999:blog-8072464059979174136.post-418092070042805892011-09-09T12:02:00.000-07:002011-09-09T12:29:40.901-07:00GHC 7.0.4 on CentOSThis is mainly a post for myself so that I can look back any time how I did it.<br />
<br />
Basically I fell in every possible hole while wandering around in the dark but I could get out of them :-)<br />
<ul><li>after downloading I configured the binary installation for x86-64. <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">configure</span></span> starts <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">ghc-pwd</span></span>, which is built with the wrong <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">glibc</span></span>-versions. Bummer.</li>
<li>found out that I have to get the source install. Downloaded and configured, it died in the middle because <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">base-4.2</span></span> was not available. Bummer.</li>
<li>so I had to install <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">ghc-6.12.3</span></span> first. Fortunately this went smoothly (binary install). With this new friend I reconfigured v7.0.4 and started building. When linking the stage1 compiler I got an error from binutils that some relocation went awry. Bummer.</li>
<li>the internets are full of hints that the system compiler (<span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">gcc-4.1</span></span>) uses the bad linker. To my luck I found a new gcc-4.4 in an amicable colleague's home directory, so I reconfigured thus:<blockquote><span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">./configure --prefix=/home/gabor --with-gcc=/home/msichel/local_x86/bin/gcc</span></span></blockquote></li>
<li>but configure told me that the shiny new <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">gcc</span></span> cannot build executables. Bummer.</li>
<li>it turned out (I had to write a <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">hello-world</span></span> to figure that out) that some <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">gcc</span></span>-internal shared libraries were not found. Luckily they came into scope with <blockquote><span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">LD_LIBRARY_PATH=/home/msichel/local_x86/lib:/opt/lsf/6.2/linux2.6-glibc2.3-x86_64/lib</span></span></blockquote></li>
<li>at this point I could smell victory, but it was still out of reach. A <a href="http://klevstul.posterous.com/haskell-ghc-702-on-centos-55">blog post</a> suggested to <span style="color: purple; font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">cp mk/build.mk.sample mk/build.mk</span></span> and edit it in two ways:</li>
<ul><li>uncomment <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">BuildFlavour = quick</span></span></li>
<li>and change to <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">GhcLibWays = v p dyn</span></span>, i.e. append "<span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">p dyn</span></span>"</li>
</ul><li>I did both, reconfigured and typed <span style="font-size: x-small;"><span style="font-family: "Courier New",Courier,monospace;">make install</span></span>.</li>
</ul>It went through without a hitch :-)<br />
<ul></ul>heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-812309118978175182011-08-21T22:58:00.000-07:002011-08-21T22:58:05.937-07:00Poor Man's Haskell KindsAfter finalizing some of my idea prototypes in <a href="http://omega.googlecode.com/">Ωmega</a>, I intend to port a part of the code to Haskell, to enjoy the speed advantages of a compiled language.<br />
<br />
Unfortunately Haskell does not support <i>user-defined kinds</i>, so I was wondering how to simulate them at least, in order to get some confidence that my type-level constructs do not drift into no-no-land.<br />
<br />
<a href="http://svn.berlios.de/svnroot/repos/al4nin/trunk/purgatory/PoorKinds.lhs">This literate haskell file</a> demonstrates how I put <i>instance constraints</i> to work, and thereby define the inference rules for well-kinded phantom type indexes. I am sure somebody has already done this, I would like to hear about it. Anyway, this almost allows me to introduce Ωmega's checked singleton types in Haskell.<br />
<br />
Sadly GHC does not yet allow instance definitions for type families, but it would be cool if somebody could provide me a workaround.heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com5tag:blogger.com,1999:blog-8072464059979174136.post-68486472359433951352011-02-10T18:45:00.000-08:002011-02-10T18:45:50.298-08:00My Thoughts about InertiaBig caveat: I am very much of a layman when it comes to physics and this is consequence of having heard elementary physics lectures more than 15 years ago.<br />
<br />
But I like the occasional book on the subject (<a href="http://en.wikipedia.org/wiki/The_Elegant_Universe">The Elegant Universe</a> comes to my mind) and am fascinated by the theoretical possibility of a grand unified theory of Nature's forces.<br />
<br />
There is a small niggling idea in my head that wants to get out from time to time, and this post is the evidence that it finally made it into the wild. (I will probably appear as a bloody idiot because of this...)<br />
<br />
Being Hungarian-born has made me somewhat receptive for advances in physics performed by the pretty smart folks coming from this small country, and already as a pupil I was taught that the "<a href="http://en.wikipedia.org/wiki/Equivalence_principle">equivalence principle</a>" (of gravitational mass and inertial mass coinciding to an amazing degree) was shown by <a href="http://en.wikipedia.org/wiki/Lor%C3%A1nd_E%C3%B6tv%C3%B6s">Eötvös</a>. This cannot be a simple coincidence but must be a fundamental thing.<br />
<br />
A completely ununderstood fundamental thing, as it appears to me. A quick googling for "inertia quantum gravity" brings up some outright lunatics and some rather exotic theory of "zero field fluctuations" causing inertia:<br />
<br />
http://www.calphysics.org/articles/PRA94.pdf<br />
http://www.calphysics.org/articles/gravity_arxiv.pdf<br />
<br />
But, electromagnetism causing the same mass as gravity (i.e. linking two of the fundamental forces with an unbelievable precision) appears very far-fetched to me.<br />
<br />
Wikipedia seems to be no help when inquiring for the <a href="http://en.wikipedia.org/wiki/Inertia#Source_of_Inertia">source of inertia</a>. <a href="http://en.wikipedia.org/wiki/Mach%27s_principle">Mach's principle</a> referenced therein, namely that the existence of the rest of the universe leads to the phenomenon of inertia does not sound right; after all, when all the other stars (galaxies etc.) would be removed <i>but the Sun</i>, would you expect that the inertia of your body suddenly would fall to almost zero?<br />
<br />
I cannot believe that modern theories of gravity (such as quantum gravity approaches) do not try to explain the equivalence of gravitational mass and inertial mass. My intuition says that this should be the first step!<br />
<br />
Now I'll begin a steep descent in the land of speculation and respectlessly mix stuff told by others with vague ideas and metaphors of mine. I won't even make effort to cite or link, but at some point I'll tell what my main idea is. Be warned: at that point probably each self-respecting physicist (that is, a person who successfully solved a differential equation about movement of a body under external force) will turn away with disgust, but okay, let it be...<br />
<br />
There is this idea that gravity is so weak in comparison to electromagnetism, because the circular (closed) strings corresponding to the graviton do not permanently bind to our three dimensional space (or four-dimensional spacetime). They are just passing through, and there is little time for them to establish the force between bodies. So, the gravitational force exerted between two glasses of red wine is very small on each other. But when they are accelerated (say, by clinking them) perceptible forces appear. So I conjecture that both forces are caused by the same mass, and by the same gravitons, but they differ in magnitude, because the gravitons <i>stay around longer</i> in the second case, so <i>as messenger particles</i> they establish a force many orders of magnitude stronger.<br />
<br />
How can they stay around longer to <a href="http://dilbert.com/dyn/str_strip/000000000/00000000/0000000/100000/10000/2000/300/112314/112314.strip.gif" title="Dilbert.com">become relevant</a>? Perhaps by traveling orthogonally to the gravitational gravitons. Okay, inertial gravitons travel (more or less) orthogonally to our space, that is, along the time axis and thus following the trajectories of the particles the matter is built of.<br />
<br />
I think it was <a href="http://en.wikipedia.org/wiki/Feynman">Feynman</a> who mentioned that an anti-particle traveling 'backwards' in time can be equated with its particle traveling forward in time. Now, what is the anti-graviton? I believe that I read sometime that it is the same as the graviton. Just like a photon is not differing from an anti-photon. So the time inversion does not change any property of the graviton. Good. We have gravitons which make a short visit in our spacetime, and vanish just as fast as they appeared, and there are those which accompany mass-like particles (even when at rest) along their trajectory in time, possibly <i>bouncing</i> back and forth <i>between earlier and later</i>. This constitutes (my IDEA!) a force between a body now and its earlier appearance in spacetime. Of course this is the same as a force between now and the <i>future</i> of the body. Actually there is a force between me and (me one second later). Or ten seconds or even a year!<br />
<br />
Two things become clear now. First we have to perform an integration (over all time destinations) to get the resulting force. And second, the force toward the past will bear a negative sign, so for stationary bodies all inertial forces will cancel out. I think this can be asserted for uniform movement too (i.e. constant velocity vector) but I did not waste any thoughts on this yet. Anyway, this is Newton's first law.<br />
<br />
Time to get to the second one. Here I want to make some further remarks. The inverse-square(-like) law should hold for inertial gravitons too, so that a longer time-span enters into the integral with a smaller effect. Kind of like the gravitational force between objects a light-second apart also decrease substantially. Second, causality is a bit smeared at the very short intervals where the forces are really relevant (Planck time?) so the reality a bit before pulls hard backwards and the reality a bit later pulls hard forward. Both look pretty much the same, differing only in the arrow of the force. I do not know whether this is essential, though.<br />
<br />
Back to Newton's second law. Imagine a stroboscope lighting a scene where a body moves, accelerated by a constant force along its movement direction. When you make a photo (with reasonable exposition time) you'll obtain a picture of several bodies, with the earlier ones nearer together, and the later ones successively more distant. Now let's declare the middle one as being <i>now</i>. Then the <i>prior</i> one is less distant than the <i>next</i> one so the force between the prior and now is bigger than the force between now and next. These do not cancel out any more. This is a consequence of the inverse-square law. Of course the stroboscope should flash with Planck frequency etc. (so that the spacetime distance is small enough), but the principle is clear: We get a resultant force that points backwards, namely the difference between the (bigger) half-integral towards the past and the (smaller) half-integral towards the future.<br />
<br />
All the time I was using the wrong word 'force' for something space-time-like (a vector with 4 components). What we perceive or measure as accelerating force is the projection of that 4 component vector into our 3-dimensional space. So I conjecture that <i>F = ma</i> is the projection of the resultant 4-force which I explained in the last paragraph to our 3 dimensions.<br />
<br />
If this little idea holds any water then it should be possible to calculate the inverse law for the 4-force. I'd bet it is inverse-cubic. If this succeeds, then the next test would be to figure out how the 4-force looks like when a relativistic (say half-lightspeed) particle is accelerated by a 3-force. Clearly the 4-speed rotates out of time, but does the the mass of the particle increase?<br />
I do not dare to think about whether we can ever get to the point where this idea gets tested in an even more comprehensive setting.<br />
<br />
But it was sure a lovely night when I was drinking that red wine with a good friend from Brasil two days ago, who dared to ask a quantum-mechanical question and received a long story as an answer, unknowingly liberating this small niggling idea from the confines of my head!heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-25258187544245842582011-01-09T12:38:00.000-08:002011-01-10T06:38:20.815-08:00Quantifiers: Dark MatterModern cosmology routinely deals with <i>dark matter</i>, a source of gravity necessary to explain certain things. In the last days I discovered a kind of dark matter in Ωmega too, and here is the related story.<br />
<br />
As we know type constructors arise when the data definition is equipped with parameters, like below:<br />
<blockquote><code>data Tree a = Tip a | Fork (Tree a) (Tree a)</code></blockquote><code>a</code> is a <i>type variable</i> and gets <i>instantiated</i> (to a type) when we want the tree to contain actual information.<br />
<br />
Actually I could have written the second recursive occurrence of <code>Tree a</code> in the <code>Fork</code> branch as <code>Tree Char</code>, and the type checker would have accepted it. Why? Because at each instantiation site the type variable <code>a</code> is created <i>fresh</i>, and can be bound to a new expression.<br />
<br />
But what is the kind of <code>a</code>? In Haskell it can only be <code>*</code>, which classifies all types, as the other possible kinds (<code>* → *</code>, etc.) do not classify types. But this kinding relation is not spelled out directly, so let's choose a more explicit definition:<br />
<blockquote><code>data Tree :: * → * where ...</code></blockquote>When talking about <code>Tree Integer</code>, then it gets pretty clear that <code>Integer</code>'s kind must be <code>*</code> and that the resulting <code>Tree Integer</code> is itself kinded by <code>*</code>.<br />
But there is a fine distinction between explicit and implicit kinding in Ωmega: in the latter case <code>a</code> is kinded by a <i>unification variable</i> instead of by <code>*</code>. The reason is that Ωmega allows us to define custom kinds, which can classify other type-like things. These are usually used for indexing of type constructors.<br />
<br />
The unification variables that are present, but hidden from the user only become manifest when we have multiple levels of data definitions, with the higher levels indexing the lower ones and some constructor function tries to bind the unification variable to different kinds. Of course that won't work and all you'll see is a very cryptic error message. The smallest example I have encountered is <a href="http://code.google.com/p/omega/issues/detail?id=70">issue 70</a>, which I will present as an example here.<br />
<blockquote><code><br />
data Pat :: *3 where<br />
Q :: Pat ~> Pat<br />
<br />
data Pat' :: Pat ~> *2 where<br />
Q' :: Pat' n ~> Pat' (Q n)<br />
<br />
data Pat'' :: Pat' p ~> *1 where<br />
Q'' :: Pat'' n ~> Pat'' (Q' n)<br />
<br />
data Pat''' :: Pat'' p ~> *0 where<br />
Q :: Pat''' n → Pat''' (Q'' n)</code></blockquote>Look at the last line, it induces these two kind equations:<br />
<blockquote><code>n = Pat'' p1<br />
Q'' n = Pat'' p2</code></blockquote>Each equality at some level induces an equality at one level up. But <code>p1</code> and <code>p2</code> are kinded by the same unification variable, <code>k</code>. Let's note the two equations with <code>k</code> in the middle:<br />
<blockquote><code>m = k = Q' m</code></blockquote>where <code>m</code> is the kind of <code>n</code>.<br />
You can see now that <code>m</code> is forced to be equal to <code>Q' m</code>, which is clearly incommensurable.<br />
The solution is clearly to spell out kinding quantifiers explicitly with type variables. Since these get instantiated to fresh copies on the fly, the above problem does not occur.<br />
<br />
So we arrive at (only showing the last definition for brevity's sake)<br />
<blockquote><code>data Pat''' :: forall (o::Pat) (p::Pat' o) . Pat'' p ~> *0 where<br />
Q :: Pat''' n → Pat''' (Q'' n)</code></blockquote>Black magic? Only when you let the kinds live in the dark!heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-85954576171180911352010-12-27T14:57:00.000-08:002010-12-27T14:57:48.322-08:00Recently Implemented Syntax ExtensionsThe alert reader must have noticed that in my <a href="http://heisenbug.blogspot.com/2010/12/zipping-through-it.html">recent post</a> I refer to a syntax extension called <span class="Apple-style-span" style="font-family: 'Helvetica Neue', Arial, Helvetica, sans-serif;">LeftList</span>, intended to model left-associative lists, which are naturally showing up in many contexts.<br />
<br />
But that's not all, I've been busy adding more goodness. After realizing that the frontend for expressions of the form <span class="Apple-style-span" style="font-family: 'Helvetica Neue', Arial, Helvetica, sans-serif;">()u</span> and <span class="Apple-style-span" style="font-family: 'Helvetica Neue', Arial, Helvetica, sans-serif;">(42)i</span> was already present, I decided to add these as <span class="Apple-style-span" style="font-family: 'Helvetica Neue', Arial, Helvetica, sans-serif;">Unit</span> and <span class="Apple-style-span" style="font-family: 'Helvetica Neue', Arial, Helvetica, sans-serif;">Item</span> syntactic extensions. I documented them in the manual, so the next release will be up-to-date documentation-wise.<br />
<br />
Today, being given some idle time, I came around to finish up the <span class="Apple-style-span" style="font-family: 'Helvetica Neue', Arial, Helvetica, sans-serif;">LeftRecord</span> extension, which is just what you would expect. Implementing it turned out to be even easier than the same process performed for <span class="Apple-style-span" style="font-family: 'Helvetica Neue', Arial, Helvetica, sans-serif;">LeftList</span>, not only because of the lessons learned, but for want of the ambiguous parsing of <span class="Apple-style-span" style="font-family: 'Helvetica Neue', Arial, Helvetica, sans-serif;">{tail; tag=val}lr</span> which does happen with <span class="Apple-style-span" style="font-family: 'Helvetica Neue', Arial, Helvetica, sans-serif;">LeftLists</span>: <span class="Apple-style-span" style="font-family: 'Helvetica Neue', Arial, Helvetica, sans-serif;">[tail; head]ll</span>.<br />
<br />
There is one itch left: adding <span class="Apple-style-span" style="font-family: 'Helvetica Neue', Arial, Helvetica, sans-serif;">LeftPair</span>s, which should be a piece of cake, and could happen anytime. And then there is a <i>pie-in-the-sky</i> enhancement request (a.k.a. <a href="http://code.google.com/p/omega/issues/detail?id=64">issue 64</a>), which is somewhat tricky, so do not expect it being done any day now.heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-42757754445848955712010-12-14T00:01:00.000-08:002010-12-14T00:24:04.364-08:00Singleton Types are the Key to Co-dependencySince the last time I wrote <a href="http://heisenbug.blogspot.com/2010/11/more-on-existentials.html">about existentials</a> I had a plenty of time to ponder how they fit into the <i>qualifier-typed typed</i> lambda calculus which de Bruijn <a href="http://alexandria.tue.nl/repository/freearticles/597608.pdf">has proposed</a>, and I am very proud of <a href="http://svn.berlios.de/viewvc/al4nin/trunk/purgatory/Kinding.omg?revision=924">implementing a formalization</a> for.<br />
<br />
The headline has already spoiled the suspense, but the interesting part is how I arrived at that assertion. It happened last night and it carries all the attributes of an <i>epiphany</i> :-)<br />
<br />
There were some anomalies that worried me about the introduction of existential qualifiers in the <a href="http://heisenbug.blogspot.com/2010/11/more-on-existentials.html">prequel post</a>:<br />
<ol><li>the treatment of patterns that are values was missing,</li>
<li>the handwavy argument how the proposition corresponding to the condition is encoded,</li>
<li>that the dependent sum binder introduced <i>two variables</i> (where lambdas only introduce one),</li>
<li>and finally that parenthesized condition after the ∃-quantor which do not seem to appear in logic textbooks.</li>
</ol>It was the first worry that kept me awake this night. Here is a prototypic definition:<br />
<blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">fac 0 = 1</span></blockquote><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">fac (1+n) = (1+n) * fac n</span></blockquote>In <a href="http://www.opendylan.org/">Dylan</a> (an object-oriented functional language) one would write the first branch of same function as<br />
<blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">define method fac (n :: singleton(0)) 1 end</span></blockquote>Here the <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><a href="http://www.opendylan.org/books/drm/Constructing_and_Initializing_Instances#singleton">singleton</a></span> function <i>returns a type</i> whose sole inhabitant is the argument to <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">singleton</span>. This analogy pushed me over the top. What if I introduced the concept of <i>co-dependency</i> in my formalization? Say,<br />
<blockquote>∃x:singleton 1 . x</blockquote>where values can be lifted up in the type realm and appear at the right-hand-side of the type judgement (:). I prefer to call this co-dependency because it is opposite to regular dependency which happens in the <i>returned expression</i>. Consider the following type-theory expression:<br />
<blockquote>λx:Int . 〈y:singleton (5*x)〉 . y</blockquote>here a universally quantified variable (x) is entering an expression which is the argument to the singleton construct giving the type to y. What does it mean? That for every x there is an y of 5 times the magnitude, which becomes the result.<br />
<br />
With this interpretation all my worries have vanished: there is just one variable added by the dependent sum quantification and the condition is now neatly tucked away on the right side of the colon!<br />
<br />
Next to come: introduce this idea into the formalization.heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com6tag:blogger.com,1999:blog-8072464059979174136.post-48704110780374366522010-12-11T04:23:00.000-08:002010-12-11T04:34:39.846-08:00Zipping through itIn my email conversation with <a href="http://coder.bsimmons.name/blog/">Brandon</a> prior to the release of <a href="http://hackage.haskell.org/package/thrist">thrist-0.2</a>, I told him that I did not come around implementing reverse thrists, and I showed how they arise naturally when doing computational passes over thrists: <span class="Apple-style-span" style="font-family: 'Helvetica Neue', Arial, Helvetica, sans-serif;">(((a, b), c), d) e (f, (g, (h, i)))</span>. He asked me whether this has anything to do with <a href="http://www.haskell.org/haskellwiki/Zipper">zippers</a>, which I answered to the affirmative, my previous ideogram being essentially a <i>thrist zipper</i>. As it maneuvers through the data structure it deconstructs the original thrist, places a new element into focus and zips together a left-associative structure behind. Visually it (kind of) corresponds to the zipper on your jacket.<br />
<br />
This post is dedicated to this versatile tool being applied to thrists to obtain an isomorphic data structure which I call the <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">ThristZipper</span>.<br />
<br />
As the ideogram demonstrates, this zipper consists of three parts:<br />
<ol><li>the left-associate thrist (usually holding the already visited portion),</li>
<li>the focus element <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">e</span>,</li>
<li>the (right-associative) thrist (usually to be iterated over).</li>
</ol>So first we have to define <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">LeftThrist</span> (this is how I prefer to call it).<br />
<blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">data LeftThrist :: (* → * → *) → * → * → * where</span></span></blockquote><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;"> LeftNil :: LeftThrist k a a</span></span></blockquote><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;"> LeftCons :: LeftThrist k a b → k b c → LeftThrist k a c</span></span></blockquote><div style="margin-bottom: 0px; margin-left: 0px; margin-right: 0px; margin-top: 0px;">Again, the types match up. Now we can define <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">ThristZipper</span>:</div><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">data ThristZipper :: (* → * → *) → * → * → * where</span></span></blockquote><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;"> Focus :: LeftThrist k a b → k b c → Thrist k c d → ThristZipper k a d</span></span></blockquote><div style="margin-bottom: 0px; margin-left: 0px; margin-right: 0px; margin-top: 0px;">It remains to define all the operations on <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">ThristZipper</span> that will make it a versatile tool.</div><div>We start with <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">zipInto</span>:</div><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">zipInto :: Thrist k a b → Maybe (ThristZipper k a b)</span></blockquote><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">zipInto Nil = Nothing</span></blockquote><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">zipInto (Cons e r) = Just (Focus LeftNil e r)</span></blockquote><div>We can similarly define <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">zipLeftInto</span>, <i>advancing</i>, <i>focus manipulation</i>, <i>maps</i>, <i>folds</i> and <i>getting out</i> on the right or in the left. These are of course left as an exercise to the reader, but I will define retract (the opposite movement from <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">advance</span>) here for good measure:</div><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">retract :: ThristZipper k a b → Maybe (ThristZipper k a b)</span></span></blockquote><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">retract (Focus LeftNil _ _) = Nothing</span></span></blockquote><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">retract (Focus (LeftCons r e') e t) = Just (Focus r e' (Cons e t))</span></span></blockquote><div>And a lot prettier in Ωmega (<a href="http://code.google.com/p/omega/source/browse/#svn/trunk/src">svn HEAD</a>):</div><div><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">retract (Focus []lt _ _) = Nothing</span></span></blockquote><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">retract (Focus [r; e']lt e t) = Just (Focus r e' [e; t]l)</span></span></blockquote><br />
PS: I definitely plan to make all this part of thrist-1.0 when it arrives. </div>heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-77413507985435671792010-12-10T15:09:00.000-08:002010-12-10T16:58:52.735-08:00The Sky was the LimitEveryone remembers Tom Petty's song <a href="http://www.chordie.com/chord.pere/www.guitaretab.com/p/petty-tom/14484.html">'Into the Great Wide Open'</a> with it's famous refrain<br />
<blockquote><span class="Apple-style-span" style="font-family: 'Helvetica Neue', Arial, Helvetica, sans-serif;"><i>The sky was the limit</i></span></blockquote>I was thinking about limits (the category theory ones) for many years now, but could never really visualize the concept. (I should really start reading <a href="http://ukcatalogue.oup.com/product/9780199237180.do">Awodey's 'Category Theory'</a> which will be my present to self at Xmas.) I tried to get hold of the related problems with a mental construction of a lazy, self-building thrist. It was clear that each element should increase the type, <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">Z</span>, <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">(S Z)</span>, <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">(S (S Z))</span>, etc. ad infinitum, so the start type would be clear: <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">Thrist Up Z ?</span>. But the <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">?</span>, let's call it the limit, is not clear at all. Anyway it would be an infinite type, not like in the simple analogy of <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">let count = 0 : count in count</span>, where <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">count :: [Int]</span> holds. As we know type checkers do not like infinite types, as it would take forever and two days to check them :-)<br />
<br />
Fortunately the sky is not a limit anymore and I came up with a solution that is nice and short even in Ωmega, which is a strict language (albeit with a <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">lazy</span> construct). Since it is only a few lines I can effortlessly reproduce it here.<br />
<blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">data Count :: Nat ~> Nat ~> * where</span></blockquote><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"> Incr :: Nat' n -> Count n (1+n)t</span></blockquote><div>The <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">Incr</span> constructor states the typing rule, namely one higher to the right than to the left. We can try it out:</div><div><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">prompt> [Incr 0v, Incr 1v, Incr 2v]l</span></span></blockquote><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">[(Incr 0v),(Incr 1v),(Incr 2v)]l : Thrist Count 0t 3t</span></span></blockquote></div><div>Not surprisingly, this is the only value of type <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">Thrist Count 0t 3t</span>. We follow the example of <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">count</span> above and write:<br />
<blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">a = [Incr 0v; lazy (shift a)]l</span></blockquote>Naturally <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">shift</span> will shift a <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">Count</span> thrist to the right, thus satisfying the type constraint of thrists, that at each joining point the left and right types must match up. The <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">lazy</span> keyword is needed here to delay the evaluation, it is however pointless in Haskell.<br />
<br />
All that remains is to write the <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">shift</span> function which will create the ominous limit type:<br />
<br />
<blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">shift :: Thrist Count n a -> Thrist Count (1+n)t a</span></span></blockquote><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;"><span class="Apple-style-span" style="font-size: x-small;">shift [Incr n; r]l = [Incr (1+n)v; lazy (shift r)]l</span></span></blockquote><div>It is probably not a surprise that the limit value is ⊥ (i.e. nonexistent), so any type will do (along the constraints of the <i>kind</i> in question). I settled with a universal type.</div><div><br />
</div><div>Now we can pattern match on <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">a</span> to see that it really grows into the sky:</div><blockquote><span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">case a of {[a,aa,aaa,aaaa; b]l -> show b}</span></blockquote><div>prints <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">"[(Incr 4v) ; ...]l"</span> thanks to <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">show</span>'s magic. The <span class="Apple-style-span" style="font-family: 'Courier New', Courier, monospace;">...</span> corresponds to the suspended computation.</div><div><br />
</div><div>Hey, it wasn't that hard at all! Where is the infinite type? It is hidden behind the existential barrier that is formed at each thrist joining point, and since it cannot escape we do not have to worry it...</div><div><br />
</div><div>Good night!</div></div>heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com0tag:blogger.com,1999:blog-8072464059979174136.post-38356807051612387872010-12-01T18:08:00.000-08:002010-12-01T18:10:07.739-08:00Es taut nichtThe subject is German, meaning "it doesn't thaw", which is rather true: as I write this we have chilly -10 °C (14 °F) and 25 cm (10 inches) snow on the ground. And it keeps snowing. I cannot remember a winter like this.<br />
<br />
But this is not the reason of my posting! Instead I have hidden a pun in there: "there is no <i>tau</i>", yes, the Greek letter (τ). Which proposition is definitely false, because as of today I succeeded to encode de Bruijn's <i>higher degree binders</i> in <a href="http://code.google.com/p/omega/">Ωmega</a>. I've fought a lot (on and off) against this fortress...<br />
<br />
The <a href="http://svn.berlios.de/viewcvs/al4nin/trunk/purgatory/Kinding.omg?pathrev=868">code is here</a>, see and comment.<br />
<br />
PS: Does anybody know a better quality URL for <a href="http://www.cedar-forest.org/forest/papers/journals-publications/jfp6-2.ps">this paper</a>?heisenbughttp://www.blogger.com/profile/11328338875953258337noreply@blogger.com1