Version 11 (modified by benl, 7 years ago) (diff)


The Pony Farm

This is where we record possible extensions to the language, or other related projects. These are kept out of the ticket database because either: we don't really know what we want yet, or we don't know how to do it. These extensions involve significant research and/or semantics work.

Fuzz testing DDC

At one time we had a 'churn' program that generated random lambda terms and fed them into the type inferencer to see what would happen. This exposed several bugs in the type inferencer, and it would be useful to have something like this again. The old code was called 'churn', and there are remnants in the 'tools' director.

Redo the exception mechanism

The exception mechanism in the source language is based around try/catch, and doesn't have a proper semantics. We should probably just use the GHC approach where the 'error' function creates an exceptional value instead of causing a side effect.

  • If we were going to treat exceptions as side effects, then perhaps we could do something like in Benton and Buchlovsky's "Semantics of an effect analysis for exceptions" paper.

Type level natural numbers

For making use of MMX/SSE/SSE2 instructions it would be nice to have type level natural numbers so that static information about array sizes can be maintained all the way through to the code generator. With this information it should be particularly easy to make the LLVM backend do something sensible with this information.

  • If we just wanted natural numbers at the type level, without constrains on them then this would be easy to add. We'd just add add them as type constructors, with a new kind 'nat'. Adding constraints would be more work.

Add monadic do expressions

We can't reuse the source-level 'do' syntax because of ambiguity in the following program:

do Just 1
   Just 2

If the do was monadic then this would return Nothing, otherwise Just 2.

Perhaps we should use a different keyword, maybe 'mdo', to invoke monadic desugaring.

Mask mutability constraints on fresh data

In a type like

 fun :: forall r1 r2
     .  Int r1 -> Int r2
     :- Mutable r2

The returned Int is fresh, that its region does not appear on the lhs of an arrow or in a closure. In this case it does not matter that the data is Mutable, and this fetter can be masked.

We'll want to use the closure information the core language for this, so make sure the core type checker works.

Mask effects on fresh data

In a type like

 fun :: forall r1 r2
     .  Int r1 -(e1 | $0)> Int r2
     :- e1 = Read r2

The effect Read r2 isn't being masked because r2 is visible in the shape of the type. However, as the data is fresh the fact that there was a read when constructing it does matter, so it can be masked.

Jared: This also causes a spurious Write effect in primString_eq, which gets it from string_flatten. The result is that string equality can't be used as a guard to a top-level function. The following code can be used as a test case.

foo () = do
    result = newString 6
    dangerPack "effect" result