This seems more like the safety of dynamic typing, the opportunity for optimization of dynamic typing, and a chance to write a lot of irritating, small unit tests for types that a proper typed language would handle automatically.

After all, here's the same "add" in Haskell (and it's properly checked):

add = (+)

The monomorphism restriction forces one type on that, unless you add a type signature. But that doesn't really matter here... Try in ghci "let add = (+); :t add" (replacing ; with a newline) and you'll get Integer -> Integer -> Integer

Try in ghci "let add = (+); :t add" (replacing ; with a newline) and you'll get Integer -> Integer -> Integer

I didn't belive you until I actually tried in ghci. Why is that so? It seems very weird to me...

http://www.haskell.org/haskellwiki/Monomorphism_restriction

Here's an explanation. In ghc you can enable -fno-monomorphism-restriction, I think.

Thanks!

But, if you write

           
            add x y = x + y
           
          

the monomorphism restriction won't apply, because it's a function binding rather than a pattern binding.

I usually just turn the MR off. (You can add :set -fno-monomorphism-restriction to your .ghci) I've been bitten by it far more times than it's actually helped.

It's a good and interesting idea, but is it really safe? Those type assertions look suspect to me - what if I had the type assertion "foo Int => Int", but foo can return an Int or, in very rare cases, a List, depending on the input value? If the checking is done solely by testing, there's obviously no way for the type checker to catch this, even if it would be an easy error to catch by conventional methods.

It's a compile time check. It does the checking by type inferencing.

I suppose I still need to figure out the finer details, but here's what I think /should/ work: assuming you know all of the types of all of the functions called in a specific function F, you can infer all of F's types. (Oh yes, these functions can have multiple types...) The type assertion just makes sure that F has at least that specific type.

The only problem would be when you don't know and can't find out the relevant types of a function... I'm not quite sure that's possible.

You do bring a valid point though:

           
            whatever 0 -> 0
whatever 1 -> 0 : nil
           
          

Is an odd function... Perhaps it has type

           
            Int => Int, List Int
           
          

This would throw the type system a little bit off balance (what if you only ever call whatever with 0, never with 1?). I suppose I'll have to think about that.

Looks interesting. If I were you I'd stop calling those = decelerations "unit tests". Rather they should be assertions of equality, used both for testing and optimization, like ghc's rewrite rules.

It's nice to be able to return multiple types. While certainly not the same as this, anonymous sum types would be cool for haskell. (tuples are anonymous product types). We've got Either, but its limited to two and doesn't have syntax sugar :)

I'll edit the article then. You can use more than just "=" in these assertions. You can use any boolean.

There are actually two ways to pass multiple values in ae:

           
            a, b
           
          

is both a and b at the same time.

           
            a; b
           
          

is a, but if something fails (for example, if a function/message isn't defined on a) it is b.

Another way of saying ; (semicolon) is with a newline:

           
            bla -> a; b
           
          

and

           
            bla ->
    a
    b
           
          

are equivalent.

The environment could be looked at as a long list of ';' (although I wouldn't/won't implement it that way).

So, this is just runtime checks? Design by contract anybody?

Actually, it's compile time checks.

And when I say compile time, I mean "the time when the code is read, before it is actually run". I don't mean that ae has to be compiled.

How do the assertions work? Like Haskell's QuickCheck or what? If that is the case, I consider that a runtime check (because it isn't statically guaranteed).

The unit tests should work like QuickCheck, yes.

If you're doing static checking of static properties, that's usually called static type checking. It sounds like you're essentially talking about a partial static typecheck prior to execution, with dynamic typechecks to ensure safety later for the bits that the static checks couldn't cover.

There's been quite a bit of research on similar systems, starting with the work on soft typing and most recently, gradual typing.

I'll read up on that. Thank you.

nothing really interesting.. Common Lisp already has those type assertions, and it can check them during compile-time, doing type inferences etc..

maybe it's done somewhat better in ae than in Common Lisp, but such statement is not inspiring:

ae makes no guarantee on what will happen if you call a function with the wrong type of input, but this usually causes the caller function to have a type mismatch, which is still signaled at compile time.