В таком виде - нет. У Вас castToBox имеет тип forall a . Nat -> Box a, то есть для любого a по выбору _вызывающего_ castToBox должна вернуть Box a. Вам же надо вернуть Box a для какого-то конкретного a, которое соответствует значению переданного числа. То есть тип castToBox должен быть Nat -> exists n . Box n - castToBox возвращает Box n для какого-то n, какого сама захочет. Проблема в том, что такого exists в хаскеле нет, поэтому нужно его как-то по другому закодировать. Один из вариантов - сделать data SomeBox where SomeBox :: Box a -> SomeBox теперь castToBox имеет тип Nat -> SomeBox, возвращает Box n для какого-то n, завернутое в SomeBox
Nat -> Box a, а надо (n : Nat) -> Box n. Это можно сделать через singletons
хм, в хаскеле case, не будет покрывать (нечестно) exists ?
Ну так да, с помощью ExistentialTypes и потом кейсу по этому типу и эмулируются экзистенциалы
Обсуждают сегодня