> 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.

Reply via email to