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
> 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).
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. 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 :-)
Keean.
_______________________________________________
bitc-dev mailing list
bitc-dev@coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev
