> I would rather have positive and natural be predicates that can be attached
> (statically or dynamically) to a value than be concrete types themselves.
I actually have a relevant situation to this, but it's a bit long and probably
derailing/not fit for the forum, and I'd risk embarrassment if the ideas are
ill thought out; but I'll say it anyway. I'd have put it in `<details>` like on
Github but I can't find a way to do something similar in RST, for now I'll just
put it in a blockquote.
> In my scripting language I've been trying to do something like this, where
> refinement types are "properties" over concrete types that you can use in
> both compile time overloading and optimized dynamic dispatch. For example the
> `Positive` property here has a predefined check of `value > 0` that is used
> in dynamic dispatch:
>
>
> # syntax is conceptual
> Positive = property(check: x => x > 0)
> foo(_: Int{Positive}) = "positive"
> foo(_: Int{Not(Positive)}) = "not positive" # without Not() dynamic
> dispatch becomes complicated
>
> x = 1{Positive} # attached to type
> foo(x) # resolves positive overload at compile time
>
> foo(1)
> # unknown at compile time if 1 is Positive or Not(Positive)
> # so this is equivalent to:
> if Positive.check(1), foo(1{Positive})
> else if Not(Positive).check(1), foo(1{Not(Positive)})
>
>
> Run
>
> It's not as freeform as pattern-based dispatch like in Erlang/Elixir or
> Haskell, but it abstracts away stuff like guard returns or
> `IllegalArgumentException`.
>
> The roadblock of implementing this has been figuring out when and how to
> efficiently store/cache properties at runtime for specific values. For
> example I would like to implement distinct types this way (properties can
> also affect type relations) but that wouldn't work with dynamic dispatch
> without the property information being kept at runtime.
>
> Macros are already implemented like this though, function types like
> `(Context, Expression, Statement, Statement, Expression) -> Statement` can
> have a property like `Meta((Any, Int, Any, Any) -> String)`, where a symbol
> with such a type would act like Nim's `macro foo(a: untyped, b: int, c:
> typed, d: untyped)`. The benefit is that this property is only considered
> during overloading and `foo` can be treated as just a regular function
> otherwise.
>
> I wouldn't know if this is correct or ergonomic or sound though as admittedly
> it isn't very far along, I'm even considering moving function signatures to a
> property which is making me suspicious of the idea.