archives

General purpose as a special case?

In another forum, I attempted to start a discussion of best languages for learning new paradigms. The idea was to identify languages that would lead a programmer to do new things, or at least learn new concepts that could be applied to working in the programmer's everyday language.

In preparation, I made a list of every paradigm I could find mention of. Then I pruned the list by asking, "Would using or not using this concept require changing how a problem is modeled?" For the remaining paradigms, I searched for the best language, with the requirement that any implementation not be just an academic toy and not be used only in special-purpose tools.

I was surprised to end up with a very short list. It could be I just did a bad job of setting criteria. But perhaps it is the case that in the space of possible paradigms, ones flexible enough for general-purpose programming inhabit a relatively tiny range?

By Wendell at 2011-12-03 00:48 | LtU Forum | 49 comments | other blogs | 12289 reads

Proofs of a type system's safety?

I was looking at linear types really hard lately. I made my own implementation of them in haskell.

It's not a good implementation. I don't think it can handle multiple linear variables at once. As well, it's probable leakier than a sack full of holes. However, my code, attached below, isn't the topic I want to talk about anyways, rather I want to use it to raise another topic: how does one prove a type system has a desired property?

What are some papers, proofs, tutorials and, books? Even just the right name to search for would be a good start. I have no clue how to prove that my system is actually safe. I don't even know what the actual theorem would look like in a formal notation. I don't even know what the formal notation would be!

P.S. Please don't poke holes in my code. It's just a rough draft of the idea. Besides I'm asking about how people prove a type system works. Of course, I haven't taken a good look at my code. I don't know how to.

P.S.S. Here's the attached code. The basic idea is there is a context variable in the type. Every time one reads or writes a variable one get's some new context variable and therefore one can't mix the past and the future or two concurrent events.

module(
(-->),
(==>),
($=),
(-\),
lmap
)where
newtype Linear context a = Linear (IORef a)
newtype Process context a = Process (IO a)
instance Functor (Process context) where
fmap f (Process x) = Process $ fmap f x
instance Monad (Process context) where
return = Process .return
(Process x) >>= f = Process (x >>= \a -> case f a of { Process p -> p })

(-->) :: Process context (Linear context a) -> (forall context1. Process context1 (Linear context1 a) -> Process context1 a -> b) -> b
(Process p) --> f = f (fmap fst w) (fmap snd w) where
w = Process $ do
(Linear r) a return (Linear r, a)

($=) :: Process context (Linear context a) -> Process context a -> (forall context1. Process context1 (Linear context1 a) -> b) -> b
(Process p) $= (Process q) = \f -> f $ Process $ do
(Linear r) x writeIORef r x
return (Linear r)
infixr 1 $=

(-\) :: (Process context (Linear context a), Process context a) -> (forall context1. Process context1 (Linear context1 a) -> b) -> b
(a,b) -\ f = ($=) a b f

lmap ::
(
Process context (Linear context a) ->
forall c.
(forall context. Process context (Linear context b) -> c) ->
c
) ->
a ->
b
lmap f x = f (Process $ fmap Linear (newIORef x)) $ \(Process p) ->
unsafePerformIO $ do
(Linear s) readIORef s

--------------------------------------------------

(==>) ::
a ->
(
Process context (Linear context a) ->
forall c.
(forall context. Process context (Linear context b) -> c) ->
c
) ->
b
x ==> f = lmap f x

--------------------------------------------------

sample = 0 ==> \count0 ->
count0 --> \count1 val0 ->
(count1, fmap (+1) val0) -\ \count2 ->
count2 --> \count3 val2 ->
count3 $= fmap (+1) val2

By Steven StewartGallus at 2011-12-03 21:03 | LtU Forum | 6 comments | other blogs | 6100 reads