Come posso dire a GHC di soddisfare un vincolo <= a livello di tipo se so che è vero in fase di esecuzione?

Aug 17 2020

Ho un tipo parametrizzato da un numero naturale n:

data MyType (n :: Nat) = MyType

Le operazioni su questo tipo hanno senso solo quando n > 0, quindi l'ho specificato come vincolo:

myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id

(Si noti che le versioni reali di queste funzioni fanno uso n, trasformandola in un valore con natVal.)

Voglio creare un tipo esistenziale ( SomeMyType) che ci consenta di scegliere un nin fase di esecuzione:

data SomeMyType where
  SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType

Per produrre valori di SomeMyType, sto scrivendo una someMyTypeValfunzione che funziona come someNatVal:

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
  | n > 0 = case someNatVal n of
      Just (SomeNat (_ :: p n)) -> Just (SomeMyType (MyType @n))
      Nothing                   -> Nothing
  | otherwise = Nothing

Questo funzionerebbe perfettamente senza il 1 <= nvincolo, ma con il vincolo ottengo il seguente errore di tipo:

• Couldn't match type ‘1 <=? n’ with ‘'True’
    arising from a use of ‘SomeMyType’

Come posso aggirare questa limitazione? Dato che l'ho verificato n > 0in fase di runtime, non mi dispiacerebbe usare un'operazione come unsafeCoercequi per convincere GHC che 1 <= nè vero, ma non posso usarla semplicementeunsafeCoerce perché perderebbe il valore a livello di tipo di n.

Qual è il modo migliore per affrontare questo problema?

Risposte

6 TikhonJelvis Aug 17 2020 at 05:21

Dopo aver cercato un po 'di più, ho trovato la risposta di Justin L a una domanda simile . Ha racchiuso la sua soluzione nel typelits-witnessespacchetto che sono stato in grado di utilizzare per risolvere questo problema in modo abbastanza pulito:

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n = someNatVal n >>= check
  where check :: SomeNat -> Maybe SomeMyType
        check (SomeNat (_ :: p n)) = case (SNat @1) %<=? (SNat @n) of
          LE Refl -> Just (SomeMyType (MyType @n))
          NLE _ _ -> Nothing

a %<=? bci consente di confrontare due numeri naturali a livello di tipo e ci fornisce un testimone per sapere se aè minore di b( LE) o meno ( NLE). Questo ci dà il vincolo in più nel LEcaso di restituire a SomeMyType, ma provare a farlo nel NLEcaso ci darebbe comunque l'errore "non può corrispondere '1 <=? N' con '' True" ".

Nota la firma del tipo esplicito per: checksenza di essa, il tipo di checkviene dedotto come check :: SomeNat -> Maybe ae otterrei il seguente errore di tipo:

• Couldn't match type ‘a’ with ‘SomeMyType’
   ‘a’ is untouchable
     inside the constraints: 'True ~ (1 <=? n)

Con la firma del tipo esplicito tutto funziona e il codice è anche (ragionevolmente) leggibile.

1 K.A.Buhr Aug 19 2020 at 05:24

Come risposta più diretta, il vincolo 1 <= nè solo un alias di tipo per 1 <=? n ~ 'True. È possibile creare in modo non sicuro un tale vincolo di uguaglianza di tipo con:

{-# LANGUAGE DataKinds, TypeOperators #-}

import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce

unsafeDeclarePositive :: p n -> (1 <=? n) :~: 'True
unsafeDeclarePositive _ = unsafeCoerce Refl

che è più o meno quello che typelits-witnessessta facendo sotto il cofano.

Con quella definizione in atto, quanto segue dovrebbe controllare il tipo:

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
  | n > 0 = case someNatVal n of
      Just (SomeNat (pxy :: p n)) ->
        case unsafeDeclarePositive pxy of
          Refl -> Just (SomeMyType (MyType @n))
      Nothing -> Nothing
  | otherwise = Nothing