A better type notation system

[ysmood]

62b8206

[winterland1989]

Well, it's not Hindley-Milner, it's haskell style notation, In Hindley-Milner there's no type class constrain, haskell's type system is based on system FC.

[ysmood]

Can Haskell write something like this?

foo :: (String a, Number | String b) => a -> b -> a

62b8206#diff-7fba45d6a4d001d6dd7d3667b877af1cR25

Is System F not a HM style type system?

[winterland1989]

Ok, I try my best to be simple, because this's a complex problem, and all you want is just haskell style type notation to help address some js document issue:

a) HM is not a notation system, it's a type infer system, it describes how to infer certain type from given types, it can infer simple type and rank-1 polymorphic type. e.g. forall

b) HM is a restricted version of System F, because System F is undecidable at some circumstance.so System F is not a HM, but then reverse holds.

c) Haskell use a heavily modified System FC type system, to infer higher rank polymorphic and kind.

d) => and :: is haskell style type notation. by writing =>, i assume you want to express some constrains on type variables, am i right ?

e) By writing Number | String b i guess you want to write a Monoid? maybe i'm wrong and you want use other polymorphic property of them, then you should define a typeclass like:

class StringOrNumber a where
  (+) :: a -> a -> a
  -- (+) is an example what kind of polymorphic property you want to use in StringOrNumber

and then write (StringOrNumber b) => ...

because from Number | String b no type system can infer what kind of polymorphic property you want to define in your function, so even system FC can't help here.

Write Number | String b as you wish, because js doesn't have a usable type system anyway, and all you want is make document better. I just want to point out that HM is not a notation system, even it was, it can't express arbitrary type constrain like Number | String b

[ysmood]

No, I don't want that. I just want to draw some ideas from HM. See the DSL part of my commit. I intend to invent a recursive way to express function type:

1. 62b8206#diff-7fba45d6a4d001d6dd7d3667b877af1cR36
2. 62b8206#diff-7fba45d6a4d001d6dd7d3667b877af1cR38

1 and 2 can be combined together, see how the foo works:

var bar = T(
  { a: String, b: Number },
  'a', 'b',
  { id: 'a', val: ['b'], foo: T({}, 'a', ['a']) }
);

[ysmood]

It's only on a draft stage, when it's implemented in the nokit, you will get a precise purpose of what I want.

[winterland1989]

ok, maybe you should invent some name on your own, something like ys type notation? Hindley-Milner is a such a classic algorithm to solve rank-1 types.

[ysmood]

I use HM to remind me of some basic type concepts.

When people mention HM, it can be a type system, not only an algorithm, and I say HM Function Type Notation which apparently means "some HM related function type notation". I don't think there's anything improper. It's just a way people talk about things. For example this article. If you think the author should change his article name to something like "Haskell like type notation", please argue with him.

I don't know what you really want from here. It's apparently a memo for myself only, not an academic paper.

[winterland1989]

Don't get me wrong, just to remind you some concept i happened to familiar with, do whatever serve you well.
Don't know the author you refer, but from all the articles i read, when people talk about HM, they do refer the classic rank-1 type inference. and type system are indeed inference algorithms. they can be written in any kind of notations. there're are tons of papers on comonad.reader or similar place.
Let's stop here, do whatever serve you well. i really mean it.