In modo informe si dice che una prova è il tipo vuoto (cioè falso)

Question

Voglio scrivere una funzione che accetta un parametro Nat come parametro e restituiscilo SOLO se questo nat non è divisibile per tre.

ad esempio:

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

Per fare questo, devo scrivere qualcosa che dicono "N non è divisibile per _3", o "Mod.Aux [N, _3, _0] è il tipo di vuoto "

come posso farlo in forma informe?

Answer 1

Il modo più semplice in questo caso particolare è probabilmente solo per utilizzare =:!= (anche se nota che è necessario un nuovo parametro del tipo):

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 

Più in generale, non è troppo difficile esprimere questo tipo di vincolo come una classe tipo:

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 

O anche, più in generale:

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 

Entrambe queste soluzioni utilizzano lo stesso meccanismo di =:!= (ad es. si basano sul fatto che il compilatore Scala non riuscirà a trovare un valore implicito se ha due candidati che non può dare la priorità).

Probabilmente tenderei ad andare con il secondo approccio, a meno che non trovassi che avevo bisogno di molti vincoli come questo per lo stesso tipo, nel qual caso il terzo potrebbe essere più pulito.