Làm thế nào bạn có thể nói rằng bằng chứng là loại trống (tức là sai)

Question

Tôi muốn viết một hàm lấy Nat làm tham số và trả về giá trị nat này nếu nat này không chia hết cho ba.

ví dụ:

def myFunction[N <: Nat](n :N)(implicit ev: /* what do I put here that say not divible by 3 ? */): N = n 

Để làm điều đó, tôi phải viết cái gì mà nói "N là không chia hết cho _3", hoặc "Mod.Aux [N, _3, _0] là loại trống "

làm cách nào tôi có thể làm điều đó trong không có hình dạng?

Answer 1

Cách đơn giản nhất trong trường hợp đặc biệt này có lẽ là chỉ để sử dụng =:!= (mặc dù lưu ý rằng bạn cần một tham số kiểu mới):

import shapeless._, nat._, ops.nat.Mod 

def myFunction[N <: Nat, R <: Nat](n: N) 
    (implicit mod: Mod.Aux[N, _3, R], neq: R =:!= _0) = n 

Tổng quát hơn, nó không phải là quá khó để diễn tả loại hạn chế như một lớp học loại:

trait NotDivBy3[N <: Nat] 

object NotDivBy3 { 
    implicit def notDivBy3[N <: Nat]: NotDivBy3[N] = new NotDivBy3[N] {} 

    implicit def notDivBy3Ambig[N <: Nat] 
    (implicit ev: Mod.Aux[N, _3, _0]): NotDivBy3[N] = unexpected 
} 

def myFunction[N <: Nat: NotDivBy3](n: N) = n 

Hoặc thậm chí tổng quát hơn:

trait DoesntHave[N <: Nat, Prop[_ <: Nat]] 

object DoesntHave { 
    implicit def doesntHave[N <: Nat, Prop[_ <: Nat]]: DoesntHave[N, Prop] = 
    new DoesntHave[N, Prop] {} 

    implicit def doesntHaveAmbig[N <: Nat, Prop[_ <: Nat]] 
    (implicit ev: Prop[N]): DoesntHave[N, Prop] = unexpected 
} 

type Mod3Is0[N <: Nat] = Mod.Aux[N, _3, _0] 
type NotDivBy3[N <: Nat] = DoesntHave[N, Mod3Is0] 

def myFunction[N <: Nat: NotDivBy3](n: N) = n 

Cả hai giải pháp này đều sử dụng cùng một máy móc như =:!= (tức là họ dựa vào thực tế là trình biên dịch Scala sẽ không tìm thấy một giá trị tiềm ẩn nếu nó có hai ứng cử viên mà nó không thể ưu tiên).

Tôi có thể có xu hướng đi theo phương pháp thứ hai, trừ khi tôi thấy rằng tôi cần rất nhiều ràng buộc như thế này cho cùng loại, trong trường hợp đó, thứ ba có thể sạch hơn.