Posted: Mar 07, 2012 11:43 am
by VazScep

Thread split from here by request. -Spinozasgalt
SpeedOfSound wrote:I discovered a new set of tinker toys.

About a year ago I ran into a serious issue with NS that is only hinted at by your mention of models above. Up against a mathematical wall and looking for a way in.
In computer science, we talk about abstract data-types rather than abstract algebras, and we talk about implementations rather than models. They amount to the same thing. In theorem proving, we use precisely the same syntactic machinery to define group theory and its models as we do to define say, the abstract data-type of sets and its implementations.

You need quite a bit of extra machinery to pull this sort of thing off and get it type-checked. In Java, you can define interfaces for your abstract types and define classes implementing those interfaces for the models. In C++, you use the keyword "abstract" explicitly for the interfaces. In ML, you have signatures and structures. If you don't have these extra bits of machinery, you are shit out of luck.

But one thing you do have in some of these languages is type-polymorphism. In Java and C#, this is called "generics". And it's pretty powerful.

I encountered a blog last year which has the snappy title "Abstract types are existential types!" I didn't read the blog at the time. The title was beautiful enough. It was declaring that when we talk in abstractions, as in abstract algebra, we are really just talking in existentials. To say that something exists is to form an abstraction and to form an abstraction is just to say that something exists.

It's basically a cool play on words. After reading it, I went ahead and used the standard intuitionistic encoding of existential quantifiers by the universal quantifier, used the fact that universal quantifiers are effectively type-polymorhism, and, using the play on words that abstraction is existence, I wrote the following program which encodes the expressive power of structure/signature and interface/implementation using rank-n type-polymorphism.

Code: Select all
{-# LANGUAGE RankNTypes, ImpredicativeTypes, ScopedTypeVariables #-}

import qualified Data.Set as S
import Data.List (insert)

-- The type of first-class abstract collections.
-- The basic idea is that abstract types have existential type, and
-- with the right extensions, "exists x. p" can be rendered as
-- "(forall a. p -> r) -> r." In this case, p is a tuple (or record)
-- containing the particular implementation of a collection. This
-- implementation is thrown to a continuation which must generalise
-- over the abstract type a. For this, we need at least rank-2
-- polymorphism, and it has to be impredicative for some reason.
-- Notice also that the type has higher-order kind, since type a has
-- kind * -> *.
type Collection r
  = ( forall a. ( forall b. Ord b => a b
                , forall b. Ord b => b -> a b -> a b
                , forall b. Ord b => a b -> [b])      -> r) -> r

list :: Collection r
list k = k ([], (:), id)

set :: Collection r
set k = k (S.empty, S.insert, S.elems)

bag :: Collection r
bag k = k ([], insert, id)

-- Silly example, pushing two lists through a collection type.
viaCollection :: (Ord a,Ord b)
                   => Collection ([a],[b]) -> ([a],[b]) -> ([a],[b])
viaCollection c (xs,ys) = c f
  where f (empty  :: forall b. Ord b => a b
          ,insert :: forall b. Ord b => b -> a b -> a b
          ,elems  :: forall b. Ord b => a b -> [b])
          = (elems $ foldr insert empty xs,
             elems $ foldr insert empty ys)
None of this is new (well, it was new to me). But it's the sort of application of a play on words that I can get behind, and, referencing the other thread, it's the sort of thing which makes me suspect that the incestuous relationship that logic has with computer science has spawned far cooler things than the incestuous relationship logic has had with philosophy.