On Tue, Jun 9, 2015 at 3:43 AM, Keean Schupke <ke...@fry-it.com> wrote:
> On 8 June 2015 at 22:03, Matt Oliveri <atma...@gmail.com> wrote:
>>
>> > As such dubl would be:
>> > dubl :: forall a . Numeric a => a -> a
>> >
>> > so 'a' could be any integer, float, real, complex etc. This includes
>> > any
>> > ranged versions of integer
>>
>>
>> No, dubl only works on ints. Take another look at the code. It
>> necessarily works on ints within a range too, because they are ints.
>
> You are picking up on inconsequential differences, I can of course write:
>
> dubl : forall a : Integer a => a -> a
As long as you recognize that I want to be able to restrict to int,
but that refinements of int would still apply.
>> This is getting annoying. You are telling me again what *you want* to
>> do, while I'm only pointing out that this is different from what I did
>> in dubl. And I believe the range type Shap has in mind is more like
>> mine, is completely unrelated to type classes, and does not require a
>> way to compute the range endpoints at runtime.
>
>
> There are two different things I am saying, and I think you are getting
> confused between them:
>
> 1. I am pointing out that two things are the same (or at least can be the
> same in a dependently typed language, or with some kind of value-lifting).
It's true that dependent types and refinement types can look very
similar, but there's a real difference. I can't explain it simply,
just point out that it causes problems in most forms of dependent type
theory, but not in Nuprl. Nuprl has an unusual set of deduction rules
that allow you to use well-typed terms (proofs) to establish that some
other term (program) has a certain type. It has some other odd stuff
too. The subtlety is why you truly lose expressiveness without this
(as a programming language; logics can do without it), and why there's
no good workaround.
As for how _you're_ planning to do value lifting, well I'm still
interested in seeing some code that does it. And the way you
interpreted range types didn't sound like lifting either, and I don't
think it could even compete with dependent types, let alone refinement
types.
So no, I don't think our two interpretations of range types are the same at all.
> 2. I also pointed out that I don't think annotating types with constraints
> is the right way to go, for reasons of code reuse, and application
> architecture.
I don't think I confused these two things you're saying. I just
objected to you talking about number 2 in response to what I was
saying about number 1. It's very hard to reach any conclusions in
discussions with you. You tend to just move from one point to another
without explanation. Will we ever find out who was understanding
Shap's range types better? Only if Shap tells us. And if I was closer,
will you learn anything from your misunderstanding? Or will you be too
busy disagreeing with me on something else? Who knows?
> This can apply to refinement types as they are. Basically I am
> saying that functions define the constraints, which you propagate back to
> the definition. Here's an example:
>
> showDie (x : (Integer a, LessThan 6 a) => a) = putStrLn x
> id x =x
> main = showDie (id 3))
>
> The constraint is propagated through id, to the literal 3, where we can test
> if 3 satisfies the constraint (its an integer less than 6). If you cannot
> get used to writing the constraints like type classes I could write them
> like this:
>
> showDie :: {x : Integer | x < 6} -> IO ()
>
> To argue for the type-class representation, we are effectively defining a
> subtype, You should read the 'LessThan' constraint as "the value of a is
> less than 6".
>
> I could also write:
>
> data Die x = Die {a : Int | a < 6}
> showDie (Die x) = putStrLn x
> main = showDie (id (Die 3))
>
> Now, I would like that the first version of showDie be possible, I am not
> (yet) banning the second with a datatype for Die :-)
Yet more partial examples get you only so far with me. I need to see a
complete example, including the polymorphic recursion you claim to be
able to define lifting with. In addition to just seeing what the heck
things like LessThan above are, I need to see how those type
classes--which sound like they should've been predicates--fit with the
type classes that sound like they should've been types.
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
