Concatenative type syntax

[brendanzab]

I'm noticing that you're using an applicative style for types, with the <> angle brackets to denote type applications. Have you thought of going completely crazy and concatenative at the type level? This would lead to the nice parallel between the type syntax and the value syntax that you see in Haskell, Idris, etc. Eg.

define possible_winner (List<Int32>, Board -> Optional<Player>):
define possible_wins (-> List<List<Int32>>):

Would be:

define possible_winner (Int32 List, Board -> Player Optional):
define possible_wins (-> Int32 List List):

Kind of reminds me of what the MLs do with 'a list, although it makes more sense in the context of a concatenative lang. Would be interested to see what universal quantification (or even pi types) would look like in that world!

[suhr]

It's not very readable. In the language I'm (very slowly) developing, there's some sugar: foo[...] is the same as (... foo). So you can write things like List[a].

This sugar is universal, so you can use it not only in types, but also in code:

map : forall a -> Some[a], (a -> b) -> Some[b]
map (maybe fun ~ maybe) =
    case 2id:
        Some,id ->
            Some[apply]
        None,_  ->
            None

You can even write something like fold[0, {+}] , though I believe 0 {+} fold is more clear and direct.

[brendanzab]

At least you're using square brackets - after many years of Rust I'm very much over the angle brackets! Hoping most newer languages dodge this syntactic bullet!

[evincarofautumn]

Yeah, I considered this a while ago (#132), and the syntax still has an opening for this notation. It’s still something I’d like to do, especially if users end up wanting to do type-level programming or factoring of type expressions (#162). I just haven’t gotten around to working on it because I haven’t figured out a lot of the details—for example, how to get the same sort of syntactic sugar that type signatures have currently, or whether/how user-defined functions are available at the type level.

You could get universal quantification by “running” a type expression on a stack of fresh type variables. For example, the type of the identity function could be dup (->) = <S...> (S... -> S...) = ∀s. s → s, where the quantifier <Var> just introduces a local variable, same as the value-level -> var; notation.

[suhr]

I actually do this for consistency. [a, b, c] is essentially (a, b, c make_array), T[a, b, c] is essentially (a, b, c make_tuple), so it makes sense to write 42 Some as Some[42] or String List as List[String].

This syntax is space dependend though, Some [42] is not the same as Some[42]. But I'm ok with having space dependent syntax.

[brendanzab]

@suhr As an aside, the overloading of Some as a type and value constructor is quite confusing - perhaps I've been spending too much time in the dependently typed world though! 😛

[suhr]

As an aside, the overloading of Some as a type and value constructor is quite confusing

My bad, it should be Option[a].

dup (->) = <S...> (S... -> S...)

It's hard to write something that will turn a b c into (a -> b) -> c without combinators or , operation.

[suhr]

By the way, I wonder that's the good way to provide type parameters. From the one side, they are just parameters, so ... String into (or ... into[String]) makes sense. From the other side, they are implicit parameters inferred by the compiler, so ... into should also work. So there's unpleasant ambiguity.

[evincarofautumn]

@brendanzab Angle brackets aren’t a problem because Kitten’s syntax generally separates types clearly from values. We just lex them as distinct tokens and parse them as brackets or operators based on whether we’re parsing a type or an expression. It doesn’t require any other hacks like a stateful parser, and it looks more familiar to people. When I don’t have a compelling reason to do things differently, my policy is to fall back on C(++).

These aren’t yet implemented, but the cost is using the “turbofish” operator ::<> (or something like it, e.g. .<>) for type arguments in expression context (drop::<Int32> instead of drop<Int32>) and wrapping operators in parentheses when using a qualified name (tensor::(⊗) instead of tensor::⊗). But I expect that the vast majority of the time, type arguments can be inferred, and operators will be used without namespace qualification.

[brendanzab]

On a purely subjective level it's the painful syntactic weight (ugly pointiness) of angle brackets that I'm objecting to, especially when working with more interesting types. Semantics-wise, using the same syntax for application at the value level and the type level is an investment in future 'aha!' moments for your users.