No defined implementation Cast ty ty

[Termina1]

For example, there is a code that does something like:

let x : Integer = 10 in the Integer (cast x)

And I get error like:

Can't cast from Integer to Integer 

Which is strange, but we could solve this with this implementation:

Cast ty ty where
    cast = id 

I encountered this problem while doing exercise for the book Type Driven Development with Idris.
I need to implement Cast interface for some custom type.

data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Abs (Expr num)
eval : (Neg num, Integral num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Abs x) = abs (eval x)

I defined it as follows:

(Integral ty, Neg ty, Cast ty num) => Cast (Expr ty) num where
    cast orig = cast (eval orig) 

But the test example from the book failed because of the reason I described earlier:

let x : Expr Integer = 6 * 3 + 12 in the Integer (cast x) 

Am I getting something wrong? Why casting from type ty to ty haven't been implemented as a part of standard library for idris?

[xekoukou]

There is no reason to cast to the same type. This is why there is no implementation.
For the remaining questions, you could ask them at the idris irc channel or the google group if there is noone at the irc channel.

[Termina1]

@xekoukou so, I think I provided a valid use case? Why do you think there is "no reason" to do this?

[xekoukou]

If your initial piece of code is given by the Book, then you would indeed need to define Cast.
If it is not, then notice that cast can be removed, since it of the type we already have.

For the same reason, cast is not necessary in your cast from Expr num to num since eval returns num.

Your last piece of code needs to be like this:

let x : Expr Integer = Add (Mul (Val 6) (Val 3)) (Val 12) in the Integer (cast x)

[mitchellwrosen]

There is no reason to cast to the same type

What if you have a function that is polymorphic, like

foo : Cast a Int => a -> Int -> Int
foo x y = cast x + y

Shouldn't you be able to pass an Int into this function?

[xekoukou]

@mitchellwrosen Yes, then you need to provide an implementation. What I meant to say is that it is uncommon and that is the reason for its non-existence.

[Melvar]

foo : Cast a Int => a -> Int -> Int

Inside this function, the only operation you can do on the argument of type a is cast it into an Int. This provides no advantage over simply taking an Int argument.

[Termina1]

@Melvar still it is strange, that you can pass anything that can be cast to int, but not Int itself

[Melvar]

It is not strange in any way; since that’s exactly what you wrote. Well, not strange beyond you writing such a function in the first place, since as I explained it doesn’t add anything over taking the desired type directly.

[mitchellwrosen]

@Melvar I think you might be painting with too wide a brush, the function I wrote is just an example. Here's a more realistic one. Say you want to generalize "show" to return one of many possible string types (pretend Idris has a similar string quandary to Haskell's):

show :: (Show a, Cast String b) => a -> b

The idea is that the caller is no longer responsible for peppering calls to cast everywhere, show will just happily cast it to whatever. It'd be inconvenient if there was no instance Cast String String in this case.

[Melvar]

That’s not what Cast is for; you’d use a dedicated IsString class. Just because you can cast from String to ty doesn’t make ty semantically a string type. (For example, Integer and Double.)

To the best of my understanding, the only reason for Cast is to centralize conversion functions so you don’t need to remember a zillion names for conversion functions.

[melted]

I think it makes sense to add it, there is only sensible way to do it and while it is a degenerate case those have tendency to be needed when one writes generic code.

15 okt. 2016 kl. 20:30 skrev Melvar Chen notifications@github.com:

That’s not what Cast is for; you’d use a dedicated IsString class. Just because you can cast from String to ty doesn’t make ty semantically a string type. (For example, Integer and Double.)

To the best of my understanding, the only reason for Cast is to centralize conversion functions so you don’t need to remember a zillion names for conversion functions.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or mute the thread.

[Termina1]

@melted do you think it is a good idea to create a PR for this change?

[david-christiansen]

I disagree with @melted here. The Cast interface is really just a way to get ahold of hacky conversions. Like @Melvar said, it's really just so we don't have to remember their names. For many implementations, cast just returns garbage output when given an input that isn't representable in the target type. For instance:

> the Integer (cast "oops")
0 : Integer
> the Nat (cast (the Int (-2)))
0 : Nat

There's no proof associated with cast to make sure it does something at all reasonable, and there's also no informal specification that people typically adhere to. Writing generic code over Cast is probably not a good idea.

I think that Cast occurring as a constraint should typically be considered a code smell. If the lack of an implementation Cast ty ty means that this style of design is difficult, then that's a good thing in my opinion.

If the library should change, then I think it should change to emit a warning when it encounters a missing Cast ty ty using error reflection. The message could read something like:

There is no implementation for Cast Int Int. Cast is intended to be used at call sites by users, rather than in library code, so this instance wouldn't make much sense.

[Termina1]

@david-christiansen I agree with you, if we're talking about Cast not being a strong guarantee while reasoning about our code, it is true, of course. However, Cast is already a part of idris standard library, so I believe this change would make its behaviour more obvious. Otherwise, may be its better to remove it and replace with something better?

[david-christiansen]

I think that there's space in the library for the occasional quick and dirty practical thing. Not all of it needs to be a shining jewel of typed perfection. We just need to be aware which parts are for quick and dirty code (like cast) and which parts are for more principled work. I think that our culture generally has that awareness, but we don't necessarily communicate it to new Idrisers well enough.