Início / coding / Perguntas / 77851992
Accepted
joel
Asked: 2024-01-21 01:23:27 +0800 CST

Argumentos apagados em construtores de tipo

  • 772

O que significa apagar um argumento em um construtor de tipo? Por exemplo

data Foo : (0 _ : Nat) -> Type where

em oposição a

data Foo : Nat -> Type where

Meu entendimento é que nada em um construtor de tipo é usado em tempo de execução, então é sempre 0. Acho que isso também leva à questão talvez mais confusa do que significaria um argumento linear em um construtor de tipo, mas isso fica para outro dia.

idris

1 respostas

  1. Best Answer

    Idris (2) é um tanto incomum porque permite correspondência direta de padrões em tipos. Construtores de tipo são tratados como Typeconstrutores de .

    finSize : Type -> Maybe Nat
finSize (Fin n) = Just n
finSize _       = Nothing

    Se você, digamos, apagou Fino argumento de , então a correspondência com um Typewith também Fin nseria napagada.

    data Fin : (0 _ : Nat) -> Type where

-- fails
-- finSize : Type -> Maybe Nat
-- finSize (Fin n) = Just n  -- have 0 copies of n, need at least 1
-- finSize _       = Nothing
-- succeeds
data Erased : Type -> Type where Erase : (0 _ : a) -> Erased a
finSize : Type -> Maybe (Erased Nat)
finSize (Fin n) = Just (Erase n)
finSize _       = Nothing
    • 1

relate perguntas