<p>I think <code>sort</code>, as presented there, isn't typeable on EAL. I can't prove that, but it doesn't work on Lamping's Abstract Algorithm without the oracle. Moreover, while the term is somewhat clever and brief, it uses very wacky strategies that are not EAL-friendly.</p>

<p>But behind this question there is a more interesting one: <em>"can a nat-sorting function be implemented in EAL"</em>? That was a very hard question back then, but now it looks pretty trivial. Yes, of course. There are many simpler ways to do it. For an example, one can just fill a Scott-encoded <code>NatSet</code> with Church-encoded <code>Nat</code>s, and then convert it to a list. Here is a complete demonstration:</p>

<pre><code>-- sort_example.mel
-- Sorting a list of Church-encoded numbers on the untyped lambda calculus
-- with terms that can be executed by Lamping's Abstract Algorithm without
-- using the Oracle. Test by calling `mel sort_example.mel`, using Caramel,
-- from https://github.com/maiavictor/caramel

-- Constructors for Church-encoded Lists 
-- Haskell: `data List = Cons a (List a) | Nil`
Cons head tail = (cons nil -&gt; (cons head (tail cons nil)))
Nil            = (cons nil -&gt; nil)

-- Constructors for Church-encoded Nats
-- Haskell: `data Nat = Succ Nat | Zero`
Succ pred = (succ zero -&gt; (succ (pred succ zero)))
Zero      = (succ zero -&gt; zero)

---- Constructors for Scott-encoded NatMaps
---- Those work like lists, where `Yep` constructors mean
---- there is a number on that index, `Nah` constructors
---- mean there isn't, and `End` ends the list.
---- Haskell: `data NatMap = Yep NatMap | Nah NatMap | End`
Yep natMap = (yep nah end -&gt; (yep natMap))
Nah natMap = (yep nah end -&gt; (nah natMap))
End        = (yep nah end -&gt; end)

---- insert :: Nat (Church) -&gt; NatMap (Scott) -&gt; NatMap (Scott)
---- Inserts a Church-encoded Nat into a Scott-encoded NatMap.
insert nat natMap    = (nat succ zero natMap)
    succ pred natMap = (natMap yep? nah? end?)
        yep? natMap  = (Yep (pred natMap))
        nah? natMap  = (Nah (pred natMap))
        end?         = (Nah (pred natMap))
    zero natMap      = (natMap Yep Yep (Yep End))

---- toList :: NatMap (Scott) -&gt; List Nat (Church)
---- Converts a Scott-Encoded NatMap to a Church-encoded List
toList natMap        = (go go natMap 0)
    go go natMap nat = (natMap yep? nah? end?)
        yep? natMap  = (Cons nat (go go natMap (Succ nat)))
        nah? natMap  = (go go natMap (Succ nat))
        end?         = Nil

---- sort :: List Nat (Church) -&gt; List Nat (Church)
---- Sorts a Church-encoded list of Nats in ascending order.
sort nats = (toList (nats insert End))

-- Test
main = (sort [1,4,5,2,3])
</code></pre>

<p>Here is the bruijn-indexed normal form of a slightly altered version of the <code>sort</code> above, which must receive <code>(x -&gt; (x x))</code> as the first argument in order to work (otherwise it doesn't have a normal form):</p>

<pre><code>λλ(((1 λλλ(((1 λλλ((1 3) (((((5 5) 2) λλ(1 ((5 1) 0))) 1) 0))) 
λ(((3 3) 0) λλ(1 ((3 1) 0)))) λλ0)) ((0 λλ(((1 λλ(((0 λλλλ(2 (
5 3))) λλλλ(1 (5 3))) λλλ(1 (4 3)))) λ(((0 λλλλ(2 3)) λλλλ(2 3
)) λλλ(2 λλλ0))) 0)) λλλ0)) λλ0)
</code></pre>

<p>Pretty simple in retrospect.</p>

CC BY-SA 3.0
2016-01-16T01:52:12.883Z
2016-01-16T01:57:53.333Z
2016-01-16T01:57:53.333Z
MaiaVictor
<p>The following λ-term, here in normal form:</p>

<pre><code>sort = (λabc.(a(λdefg.(f(d(λhij.(j(λkl.(k(λmn.(mhi))l))
       (h(λkl.l)i)))(λhi.(i(λjk.(bd(jhk)))(bd(h(λjk.(j
       (λlm.m)k))c)))))e))(λde.e)(λde.(d(λfg.g)e))c))
</code></pre>

<p>Implements a sorting algorithm for church-encoded lists. That is, the result of:</p>

<pre><code>sort (λ c n . (c 3 (c 1 (c 2 n)))) β→ (λ c n . (c 1 (c 2 (c 3 n))))
</code></pre>

<p>Similarly,</p>

<pre><code>sort_below = λabcd.a(λef.f(λghi.g(λj.h(λkl.kj(ikl)))(hi))e(λgh.h))
            (λe.d)(λe.b(λf.e(f(λghi.hg)(λgh.cfh))))
</code></pre>

<p>Also implements sorting for the same lists as above, except you must provide an additional argument with a limit for the numbers it will consider:</p>

<pre><code>sort_below 4 [5,1,3,2,4] → [1,2,3]
</code></pre>

<p>I am trying to determine whether those terms are typeable on elementary affine logic. Since I don't know any EAL type-checker publicly available, this is proving a harder task than I expected. Is there a type for <code>sort</code> in elementary affine logic?</p>

CC BY-SA 3.0
2015-08-29T12:51:43.047Z
Does it have an "ordinary" type? What happens if you plug it into Haskell?
Andrej Bauer
CC BY-SA 3.0
2015-08-29T12:53:15.090Z
And another question (the term is too big for me to stare at it): does any bound variable ever get mentioned more than once? Hmm, `b` is like that is it not?
Andrej Bauer
CC BY-SA 3.0
2015-08-29T14:11:57.640Z
I agree with Andrej, the terms are unreadable as such. What algorithms do they implement? Some [integer sorting not based on comparison](https://en.wikipedia.org/wiki/Integer_sorting)? What EAL-based typing system are you considering? The naive one (no subject reduction) or the one by [Coppola, Dal Lago and Ronchi](http://arxiv.org/pdf/0809.0195.pdf)? Are they typable in System F, e.g. $sort:\mathsf{NatList}\to\mathsf{NatList}$, where $\mathsf{NatList}:=\forall X.(\mathsf{Nat}\to X\to X)\to X\to X$?  If not, then there is no hope they are typable in any EAL-based system.
Damiano Mazza
CC BY-SA 3.0
2015-08-29T14:16:33.553Z
Some bound variables definitely get mentioned more than once, but I guess that isn't a restriction. For better visualization, [here is a haskellized version](http://lpaste.net/139825) of the term.
MaiaVictor
CC BY-SA 3.0
2015-08-29T14:18:38.407Z
@DamianoMazza wait, what you said about System-F is true? Then how come there are some terms on my wiki that aren't typeable in Haskell (at least I think so - GHC complains about infinite types), but my optimal evaluator can normalize them perfectly fine? An example being [zipWith](http://stackoverflow.com/questions/29885983/infinite-type-error-when-defining-zip-with-foldr-only-can-it-be-fixed). Yes, the algorithm is pretty simple, it just scans the array linearly taking the `pred` of each num - when it reaches 0, it outputs the number. Two ways to do the same thing without recursion.
MaiaVictor
CC BY-SA 3.0
2015-08-29T14:55:49.510Z
Yes, this is because there is a forgetful functor $(\cdot)^-$ from EAL to System F (or to simple types, if you do not use polymorphism) such that if $t:A$ in EAL, then $t^-:A^-$ in System F. The fact that your simplified evaluator works is not inconsistent with this: what makes Lamping's algorithm work without brackets and croissants is a *stratification* property of terms, which is purely structural and independent of types: there are untypable terms (in System F, EAL, Haskell or whatever) which are stratified. I guess your term must fall in this class.
Damiano Mazza
CC BY-SA 3.0
2015-08-29T15:30:57.773Z
Ah, I thought EAL captured precisely the class of terms which can be ran without the oracle. That makes more sense, now. I still don't know whether those simple λ-terms that are defined with folds instead of recursion always work with the abstract algo but now you're making me think not, indeed.
MaiaVictor
CC BY-SA 3.0
2015-08-31T10:18:00.003Z
Maybe these comments can be turned into an answer?
Andrej Bauer
CC BY-SA 3.0
2017-07-04T15:39:12.080Z
Very interesting question!
Tayfun Pay
CC BY-SA 3.0
2017-07-04T17:51:04.860Z
@TayfunPay thanks, how did you get here?
MaiaVictor
CC BY-SA 3.0
2017-07-04T18:57:32.717Z
While reading through questions. :-)
Tayfun Pay
<lo.logic><lambda-calculus><type-systems>
Is `sort` typeable on elementary affine logic?
MaiaVictor
# Is `sort` typeable on elementary affine logic?

(Asked by: username_0 on 2015-08-29)

The following λ-term, here in normal form:
sort = (λabc.(a(λdefg.(f(d(λhij.(j(λkl.(k(λmn.(mhi))l))
       (h(λkl.l)i)))(λhi.(i(λjk.(bd(jhk)))(bd(h(λjk.(j
       (λlm.m)k))c)))))e))(λde.e)(λde.(d(λfg.g)e))c))

Implements a sorting algorithm for church-encoded lists. That is, the result of:
sort (λ c n . (c 3 (c 1 (c 2 n)))) β→ (λ c n . (c 1 (c 2 (c 3 n))))

Similarly,
sort_below = λabcd.a(λef.f(λghi.g(λj.h(λkl.kj(ikl)))(hi))e(λgh.h))
            (λe.d)(λe.b(λf.e(f(λghi.hg)(λgh.cfh))))

Also implements sorting for the same lists as above, except you must provide an additional argument with a limit for the numbers it will consider:
sort_below 4 [5,1,3,2,4] → [1,2,3]

I am trying to determine whether those terms are typeable on elementary affine logic. Since I don't know any EAL type-checker publicly available, this is proving a harder task than I expected. Is there a type for sort in elementary affine logic?

**Tags:** lo.logic, lambda-calculus, type-systems
> **Comments:**
> **username_1**: Does it have an "ordinary" type? What happens if you plug it into Haskell?  
> **username_1**: And another question (the term is too big for me to stare at it): does any bound variable ever get mentioned more than once? Hmm, `b` is like that is it not?  
> **username_2**: I agree with Andrej, the terms are unreadable as such. What algorithms do they implement? Some [integer sorting not based on comparison](https://en.wikipedia.org/wiki/Integer_sorting)? What EAL-based typing system are you considering? The naive one (no subject reduction) or the one by [Coppola, Dal Lago and Ronchi](http://arxiv.org/pdf/0809.0195.pdf)? Are they typable in System F, e.g. $sort:\mathsf{NatList}\to\mathsf{NatList}$, where $\mathsf{NatList}:=\forall X.(\mathsf{Nat}\to X\to X)\to X\to X$?  If not, then there is no hope they are typable in any EAL-based system.  
> **username_0**: Some bound variables definitely get mentioned more than once, but I guess that isn't a restriction. For better visualization, [here is a haskellized version](http://lpaste.net/139825) of the term.  
> **username_0**: @DamianoMazza wait, what you said about System-F is true? Then how come there are some terms on my wiki that aren't typeable in Haskell (at least I think so - GHC complains about infinite types), but my optimal evaluator can normalize them perfectly fine? An example being [zipWith](http://stackoverflow.com/questions/29885983/infinite-type-error-when-defining-zip-with-foldr-only-can-it-be-fixed). Yes, the algorithm is pretty simple, it just scans the array linearly taking the `pred` of each num - when it reaches 0, it outputs the number. Two ways to do the same thing without recursion.  
> **username_2**: Yes, this is because there is a forgetful functor $(\cdot)^-$ from EAL to System F (or to simple types, if you do not use polymorphism) such that if $t:A$ in EAL, then $t^-:A^-$ in System F. The fact that your simplified evaluator works is not inconsistent with this: what makes Lamping's algorithm work without brackets and croissants is a *stratification* property of terms, which is purely structural and independent of types: there are untypable terms (in System F, EAL, Haskell or whatever) which are stratified. I guess your term must fall in this class.  
> **username_0**: Ah, I thought EAL captured precisely the class of terms which can be ran without the oracle. That makes more sense, now. I still don't know whether those simple λ-terms that are defined with folds instead of recursion always work with the abstract algo but now you're making me think not, indeed.  
> **username_1**: Maybe these comments can be turned into an answer?  
> **username_3**: Very interesting question!  
> **username_0**: @TayfunPay thanks, how did you get here?  
> **username_3**: While reading through questions. :-)  

---

## 1 answers

### Answer by username_0 on 2016-01-16. Score: 3

I think sort, as presented there, isn't typeable on EAL. I can't prove that, but it doesn't work on Lamping's Abstract Algorithm without the oracle. Moreover, while the term is somewhat clever and brief, it uses very wacky strategies that are not EAL-friendly.
But behind this question there is a more interesting one: "can a nat-sorting function be implemented in EAL"? That was a very hard question back then, but now it looks pretty trivial. Yes, of course. There are many simpler ways to do it. For an example, one can just fill a Scott-encoded NatSet with Church-encoded Nats, and then convert it to a list. Here is a complete demonstration:
-- sort_example.mel
-- Sorting a list of Church-encoded numbers on the untyped lambda calculus
-- with terms that can be executed by Lamping's Abstract Algorithm without
-- using the Oracle. Test by calling `mel sort_example.mel`, using Caramel,
-- from https://github.com/maiavictor/caramel

-- Constructors for Church-encoded Lists 
-- Haskell: `data List = Cons a (List a) | Nil`
Cons head tail = (cons nil -> (cons head (tail cons nil)))
Nil            = (cons nil -> nil)

-- Constructors for Church-encoded Nats
-- Haskell: `data Nat = Succ Nat | Zero`
Succ pred = (succ zero -> (succ (pred succ zero)))
Zero      = (succ zero -> zero)

---- Constructors for Scott-encoded NatMaps
---- Those work like lists, where `Yep` constructors mean
---- there is a number on that index, `Nah` constructors
---- mean there isn't, and `End` ends the list.
---- Haskell: `data NatMap = Yep NatMap | Nah NatMap | End`
Yep natMap = (yep nah end -> (yep natMap))
Nah natMap = (yep nah end -> (nah natMap))
End        = (yep nah end -> end)

---- insert :: Nat (Church) -> NatMap (Scott) -> NatMap (Scott)
---- Inserts a Church-encoded Nat into a Scott-encoded NatMap.
insert nat natMap    = (nat succ zero natMap)
    succ pred natMap = (natMap yep? nah? end?)
        yep? natMap  = (Yep (pred natMap))
        nah? natMap  = (Nah (pred natMap))
        end?         = (Nah (pred natMap))
    zero natMap      = (natMap Yep Yep (Yep End))

---- toList :: NatMap (Scott) -> List Nat (Church)
---- Converts a Scott-Encoded NatMap to a Church-encoded List
toList natMap        = (go go natMap 0)
    go go natMap nat = (natMap yep? nah? end?)
        yep? natMap  = (Cons nat (go go natMap (Succ nat)))
        nah? natMap  = (go go natMap (Succ nat))
        end?         = Nil

---- sort :: List Nat (Church) -> List Nat (Church)
---- Sorts a Church-encoded list of Nats in ascending order.
sort nats = (toList (nats insert End))

-- Test
main = (sort [1,4,5,2,3])

Here is the bruijn-indexed normal form of a slightly altered version of the sort above, which must receive (x -> (x x)) as the first argument in order to work (otherwise it doesn't have a normal form):
λλ(((1 λλλ(((1 λλλ((1 3) (((((5 5) 2) λλ(1 ((5 1) 0))) 1) 0))) 
λ(((3 3) 0) λλ(1 ((3 1) 0)))) λλ0)) ((0 λλ(((1 λλ(((0 λλλλ(2 (
5 3))) λλλλ(1 (5 3))) λλλ(1 (4 3)))) λ(((0 λλλλ(2 3)) λλλλ(2 3
)) λλλ(2 λλλ0))) 0)) λλλ0)) λλ0)

Pretty simple in retrospect.


---

