Блог

Главная - Вопросы по программированию - Интеллектуальный конструктор для кортежа в Idris

Интеллектуальный конструктор для кортежа в Idris

#haskell #idris

#haskell #idris

Вопрос:

Я начал читать главу 6 «Разработка на основе типов с помощью Idris» и попытался написать интеллектуальный конструктор для кортежного вектора.

 TupleVect : Nat -> Type -> Type
TupleVect Z _ = ()
TupleVect (S k) a = (a, TupleVect k a)

someValue : TupleVect 4 Nat
someValue = (1,2,3,4,())

TupleVectConstructorType : Nat -> Type -> Type
TupleVectConstructorType n typ = helper n
  where
    helper : Nat -> Type
    helper Z = TupleVect n typ
    helper (S k) = typ -> helper k

tupleVect : (n : Nat) -> (a : Type) -> TupleVectConstructorType n a
tupleVect Z a = ()
tupleVect (S Z) a = val => (val, ())
tupleVect (S (S Z)) a = val2 => val1 => (val2, val1, ())
-- ??? how to create tupleVect (S k) a

Как создать конструктор для произвольного k?

Ответ №1:

В основном идея @Matthias Berndt. Обратный отсчет стрелок, которые нужно добавить, делая конечный кортеж длиннее. Для этого нам нужно получить доступ к более разрешительному помощнику из TupleVectType .

 TupleVectType' : Nat -> Nat -> Type -> Type
TupleVectType' Z n a = TupleVect n a
TupleVectType' (S k) n a = a -> TupleVectType' k (S n) a

TupleVectType : Nat -> Type -> Type
TupleVectType n = TupleVectType' n Z

tupleVect : (n : Nat) -> (a : Type) -> TupleVectType n a
tupleVect n a = helper n Z a ()
    where
        helper : (k, n : Nat) -> (a : Type) -> (acc : TupleVect n a)
            -> TupleVectType' k n a
        helper Z n a acc = acc
        helper (S k) n a acc = x => helper k (S n) a (x, acc)

someValue2 : TupleVect 4 Nat
someValue2 = (tupleVect 4 Nat) 4 3 2 1

Хотя обратите внимание, что это приведет к v2 => v1 => (v1, v2, ()) , а не v2 => v1 => (v2, v1, ()) к тому, что первое лучше соответствует рекурсивному определению TupleVect (S k) a = (a, TupleVect k a) .

Комментарии:

1. Хорошее решение. Но это должно быть возможно упростить. helper a параметр type не нужен, потому что вы можете просто использовать a из области видимости. То же самое касается TupleVectType' , который вы можете просто объявить в tupleVect where предложении ‘s. Тогда есть k in helper . Если вы переименуете n переменную в tupleVect to m , то k это просто m - n и, следовательно, избыточно. К сожалению, я просто не смог скомпилировать код после внесения этих изменений :-/

2. @MatthiasBerndt a действительно избыточен. TupleVectType' должно быть явным, чтобы helper можно было получить к нему доступ. Использование m - n должно быть minus m n таким, чтобы вам не приходилось иметь дело с LTE доказательством, но вам все равно пришлось бы иметь дело с другими доказательствами и некоторыми rewrite s, так что вариант with k просто проще вводить (в смысле клавиатуры и системы типов :-)), хотя и не является строго необходимым.

Ответ №2:

Я почти ничего не знаю об Idris, за исключением того, что это зависимый типизированный язык, подобный Haskell. Но я нахожу эту проблему интригующей, поэтому я попробовал.

Очевидно, что здесь вам нужно рекурсивное решение. Моя идея состоит в том, чтобы использовать дополнительный параметр f , который накапливает val1 .. val_n параметры, которые функция съела до сих пор. При достижении базового f варианта возвращается.

 tupleVectHelper Z a f = f
tupleVectHelper (S n) a f = val => tupleVectHelper n a (val, f)

tupleVect n a = tupleVectHelper n a ()

Я понятия не имею, работает ли это, и я еще не понял, как написать тип tupleVectHelper , но я попытался выполнить замены вручную для n = 3 , и, похоже, это работает на бумаге, хотя результирующий кортеж задом наперед. Но я думаю, что это не должно быть слишком сложно исправить.

Надеюсь, это поможет!