Algoritmo de unificação infere tipos muito concretos
-
22-12-2019 - |
Pergunta
Eu estava tentando criar tuplas de tamanho n em Idris:
module NTuple
data Tuple : Vect n Type -> Type where
EmptyTuple : Tuple Nil
TupleItem : a -> Tuple types -> Tuple (a :: types)
mapN : {types : Vect n Type} -> (i : Fin (S n)) -> (a -> b) -> Tuple (insertAt i a types) -> Tuple (insertAt i b types)
mapN fZ f (TupleItem x xs) = TupleItem (f x) xs
mapN (fS i) f (TupleItem x xs) = TupleItem x (mapN i f xs)
Mas estou recebendo este erro na última linha:
When elaborating left hand side of mapN: When elaborating an application of NTuple.mapN: Can't unify Tuple (a :: types) with Tuple (insertAt (fS i) a types) Specifically: Can't unify a :: types with insertAt (fS i) a types
Existe uma maneira de fazer essa função funcionar?
Solução
O problema é que insertAt (FS i) a types
não pode ser reduzido sem saber nada sobre types
.Se soubéssemos types = t :: ts
então poderia ser reduzido a t :: insertAt i ts
.
Mas no segundo caso de mapN
, nós fazer saiba disso types
é exatamente dessa forma:
- Nosso primeiro argumento é
FS i
- Implicando
n = S m
para algunsm
... - Significando nosso implícito
types
argumento tem tipoVect (S m) Type
- O que significa que é da forma
t :: ts
!
Assim que apontarmos isso para Idris, ele ficará feliz em reduzir insertAt (FS i) a types
e assim, seu código verifica:
mapN : {types : Vect n Type} -> (i : Fin (S n)) -> (a -> b) -> Tuple (insertAt i a types) -> Tuple (insertAt i b types)
mapN FZ f (TupleItem x xs) = TupleItem (f x) xs
mapN {types = _ :: _} (FS i) f (TupleItem x xs) = TupleItem x (mapN i f xs)
mapN {types = []} (FS i) _ _ = absurd i
Licenciado em: CC-BY-SA com atribuição
Não afiliado a StackOverflow