Type Synonyms

[trans]

So today I had a pretty radical idea for type signatures... a little background first...

I have been mulling over the idea of a language much like Kitten for years now. Unlike Kitten however I planned to build it bottom-up in Assembly based on its Forth roots, as opposed to Kitten which is top-down from its Haskell roots. (Hope that's a fair characterization.)

In playing with the design for my language I needed to figure out a notation for specifying type signatures. One of the things I've always tended to dislike about type signatures is when they are long they can overshadow/obsure the definition. And that gets especially bad when where clauses are introduced (which I noticed you mentioned in your slides as something to be added to Kitten in the future.) Also, I've been hopeful signatures might eventually be inferred, with no need to explicitly provide them. But I decided that could wait, and at first at least they would be required. So, for these reasons I decided to keep the type signatures separated in a fashion similar to Haskell, rather than having them embedded in the head of the word definitions. Something like,

:: Int32 Int32 -> Int32 ;
: foo ... ;  

And that seemed pretty good. Then I got to thinking that there might be other methods with the same signature, so instead of repeating the same signature over and over, just have the signature apply to each definition after it (until the next signature).

:: Int32 Int32 -> Int32 ;
: foo ... ;  
: bar ... ;  

So even better. I really like this as it saves typing and is very clean. But it has one little problem. It forces words to be defined together and thus limits the programmers options in laying out their code.

And that's when it hit me. How do we make things reusable? We give them names. So now I am looking at something like,

:: intop Int32 Int32 -> Int32 ;

: foo intop ... ;  
: bar intop ... ;  

Or perhaps,

typesig: intop Int32 Int32 -> Int32 ;

intop: foo ... ;  
intop: bar ... ;  

While I find it a bit hard to put names to type signatures, this just seems like an abstraction that's too good to pass up. And bonus! Adding where clauses to the signatures won't further clutter word definitions.

And so having had this idea, for my very similar (idea of a) language, I though you might be interested.

[evincarofautumn]

Not so radical—these are type aliases. :)

In Haskell:

type IntOp = Int -> Int -> Int
foo, bar :: IntOp
foo = …
bar = …

Heck, even in C++, kinda:

typedef int intop(int, int);
intop foo, bar;
int foo(int x, int y) { return x + y; }
int bar(…) { … }

Kitten currently doesn’t allow these for definitions, but you’re right—it should. It will probably look like this:

type synonym IntOp (Int32, Int32 -> Int32)
define foo IntOp { … }
define bar IntOp { … }

[trans]

LOL. Yeah, it didn't occur to me that b/c of Lambda calculus one could just define the whole signature as a new type. But of course, its obvious now that you point it out.

I definitely will be making something like the "Haskell Way" the way to do it in my language. But I also want to be able to break out the code so that it can flow downwards more easily and potentially handle constraints without resorting to names, making it more Forth like.

:: IntOp -> Int32 
  Int32 0 >
  Int32

It's kind of like a word definition where what's returned is the type signature. I might even separate input signatures from return signatures. At least that's the idea. Have to think it all through and see if it works.

Kitten currently doesn’t allow these for definitions, but you’re right—it should. It will probably look like this

Not?

type IntOp (Int32, Int32 -> Int32)
define foo (IntOp): ...
define bar (IntOp): …

Did I miss something with the { ... } notation? (Alternative to indention, got it.)

Also, skimming through the slides again, I noticed traits sort of had a familiarity to all this.

[trans]

In the slides, I see you are planning to add type constraints (where clauses). What so you think of limiting those to type definitions? I think it would keep code cleaner in general and encourage the use of types.

[evincarofautumn]

Constraints are actually part of type quantifiers (bounded polymorphism). I figure the notation will be basically like in the talk:

define concat<T> (List<T> -> T) where (zero<T>, (+)<T>)
             ^^^                ^^^^^^^^^^^^^^^^^^^^^^^ quantifier
                 ^^^^^^^^^^^^^^ quantified type

This says to the typechecker “When you instantiate this type, check that matching instances of foo and bar exist”. You’ll be able to use these in type definitions, but I see no reason to disallow them in the type signatures of words. You shouldn’t have to create a separate type for each new generic word.