Como posso dizer ao GHC para satisfazer uma restrição de nível de tipo <= se eu sei que é verdade em tempo de execução?

Aug 17 2020

Eu tenho um tipo parametrizado por um número natural n:

data MyType (n :: Nat) = MyType

As operações neste tipo só fazem sentido quando n > 0, portanto, especifiquei isso como uma restrição:

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

(Observe que as versões reais dessas funções são usadas n, transformando-as em um valor com natVal.)

Eu quero criar um tipo existencial ( SomeMyType) que nos permite escolher um nem tempo de execução:

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

Para produzir valores de SomeMyType, estou escrevendo uma someMyTypeValfunção que funciona como 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

Isso funcionaria perfeitamente sem a 1 <= nrestrição, mas com a restrição, recebo o seguinte erro de tipo:

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

Como posso contornar essa limitação? Como verifiquei isso n > 0em tempo de execução, não me importaria de usar uma operação como unsafeCoerceesta para convencer o GHC de que 1 <= né verdade - mas não posso simplesmente usar unsafeCoerceporque isso perderia o valor de nível de tipo de n.

Qual é a melhor maneira de lidar com isso?

Respostas

6 TikhonJelvis Aug 17 2020 at 05:21

Depois de bisbilhotar um pouco mais, encontrei a resposta de Justin L para uma pergunta semelhante . Ele embrulhou sua solução no typelits-witnessespacote que pude usar para resolver este problema de forma bastante limpa:

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 %<=? bpermite-nos comparar dois números naturais de nível de tipo e nos dá uma testemunha se aé menor que b( LE) ou não ( NLE). Isso nos dá a restrição extra no LEcaso de retornar a SomeMyType, mas tentar fazer isso no NLEcaso ainda nos daria o erro "não é possível combinar '1 <=? N' com '' Verdadeiro '".

Observe a assinatura de tipo explícita para check- sem ela, o tipo de checké inferido como check :: SomeNat -> Maybe ae eu obteria o seguinte erro de tipo:

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

Com a assinatura de tipo explícita, tudo funciona e o código é (razoavelmente) legível.

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

Como uma resposta mais direta, a restrição 1 <= né apenas um alias de tipo para 1 <=? n ~ 'True. Você pode criar de forma insegura essa restrição de igualdade de tipo com:

{-# LANGUAGE DataKinds, TypeOperators #-}

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

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

que é mais ou menos o que typelits-witnessesestá acontecendo nos bastidores.

Com essa definição em vigor, o seguinte deve verificar o 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