These are chat archives for fthomas/refined

23rd
Aug 2015
Miles Sabin
@milessabin
Aug 23 2015 09:38
What does Int @@ Positive dealias to?
Frank S. Thomas
@fthomas
Aug 23 2015 12:17
@milessabin @@ is shapeless.@@ and Positive is just trait Positive, so that would be Int with Tagged[Positive]
Miles Sabin
@milessabin
Aug 23 2015 12:21
Oh, OK, well in that case it's definitely a refinement.
In the SLS sense.
Hiding it behind an alias doesn't stop it from being a refinement ... that's what I was getting at when I said that your definition was only capturing syntactic aspects.
If you were to dig into the type via the macro/reflection API you'd see an AliasTypeRef wrapping a RefinedType ... or something like that ...
I think your usage in the library matches the usage in the SLS very well ... in both cases we're further constraining a base type.
And via singleton types we get to constrain the type to one which only has inhabitants which satisfy particular value level predicates.
So I think the usage all round is consistent with the usage in the literature.
Miles Sabin
@milessabin
Aug 23 2015 12:33

The wikipedia article you link to says this about refinement types,

In type theory, a refinement type[1][2][3] is a type endowed with a predicate which is assumed to hold for any element of the refined type. Refinement types can express preconditions when used as function arguments or postconditions when used as return types: for instance, the type of a function which accepts natural numbers and returns natural numbers greater than 5 may be written as f: \mathbb{N} \rarr {n: \mathbb{N} | n > 5}. Refinement types are thus related to behavioral subtyping.

I think that's completely consistent with the notion of refinement in the SLS.
Frank S. Thomas
@fthomas
Aug 23 2015 12:34
Ok, I think I understand that this is true for @@. But there is also the case class Refined[T, P](t: T) value class that I added for better type inference when using an alias like type PositiveInt = Int Refined Positive. Since Refined[T, P] is not a subtype of Tit is definitely not a refinement in the SLS sense
Miles Sabin
@milessabin
Aug 23 2015 12:35
Well, perhaps, but I think you're being over cautious here.
Like I said, I think that SLS refinements are refinements in the sense described in the wikipedia article (which is a good short characterization IMO).
If you have some additional types which are not SLS refinements but which also mesh with the spirit of the idea of "refinement type" (ie. by encoding refinements as non-SLS refinements) then that seems fine too.
If you really wanted to be picky you might say that Refined is an encoding of a refinement type whereas an SLS refinement is an actual refinement type.
But TBH I don't think that would add any clarity.
Miles Sabin
@milessabin
Aug 23 2015 12:41
FWIW, @odersky is very familiar with the literature and I would be extremely surprised if he had used the term refinement in the SLS in a completely idiosyncratic way.
Frank S. Thomas
@fthomas
Aug 23 2015 12:41
I'm convinced. I'll remove that section from the README.
Miles Sabin
@milessabin
Aug 23 2015 12:41
:thumbsup:
Frank S. Thomas
@fthomas
Aug 23 2015 12:43
I don't doubt that he is, but I'm not. I wasn't really sure that my usage of that term was technically correct
Miles Sabin
@milessabin
Aug 23 2015 12:44
I think it is :-)
Frank S. Thomas
@fthomas
Aug 23 2015 12:44
Thanks, Miles, for the clarification. That was extremely helpful!
Miles Sabin
@milessabin
Aug 23 2015 12:45
It's consistent with the usage in Liquid Haskell, right?
:-)
BTW, are you going to ICFP?
Frank S. Thomas
@fthomas
Aug 23 2015 12:46
Yes, should be.
No, I'm not going. Where is that?
Miles Sabin
@milessabin
Aug 23 2015 12:46
Vancouver this year.
Frank S. Thomas
@fthomas
Aug 23 2015 12:47
Ok, then definitely not.