Здравствуйте, deniok, Вы писали:

D>Почему неизвестно? Определение же доступно.
D>

D>open import Data.List
D>open import Data.Nat
D>open import Relation.Binary.PropositionalEquality

D>length-zipWith : {A B C : Set}(f : A → B → C)(xs : List A)(ys : List B) → 
D>                  length xs ≡ length ys → length (zipWith f xs ys) ≡ length xs
D>length-zipWith f [] [] _ = refl
D>length-zipWith _ [] (_∷_ _ _) ()
D>length-zipWith _ (_∷_ _ _) [] ()
D>length-zipWith f (x ∷ xs) (y ∷ ys) e = cong suc (length-zipWith f xs ys (cong pred e))
D>

Странно, кстати, что здесь этого нет. Хорошая курсовая — дописать сюда всякий подобный length-reasoning на равенство и неравенство про все стандартные списочные функции.

Здравствуйте, deniok, Вы писали:

D>Почему неизвестно? Определение же доступно.

Да, действительно. Вот вариант на Идрисе, ближе к обсуждавшемуся zip'у:

myzip : (l : List a) -> (r : List a) -> length l = length r -> List (a,a)
myzip [] [] _ = []
myzip (x::xs) (y::ys) e = (x,y) :: myzip xs ys (cong {f = pred} e)

lenZip : (l : List a) -> (r : List a) -> (e: length l = length r) ->  length (myzip l r e) = length l
lenZip [] [] _ = refl
lenZip (x::xs) (y::ys) e = cong $ lenZip xs ys (cong e)

Здравствуйте, D. Mon, Вы писали:


DM>Да, действительно. Вот вариант на Идрисе, ближе к обсуждавшемуся zip'у:
DM>

DM>lenZip (x::xs) (y::ys) e = cong $ lenZip xs ys (cong e)

Ну да, правило конгруэнтности (x ≡ y → f x ≡ f y) — большое подспорье в спортивном и промышленном ризонинге.

Здравствуйте, C.A.B, Вы писали:

VD>>В нем типы можно будет определять самостоятельно. В такие типы можно будет вносить все что душа пожелает.
CAB>В чём отличие от создания классов?

Разницу между добавлением в язык классов и созданием конкретного класса представляешь? Вот это она и есть.

Мы делаем мета-сисстему.

Класс – это конкретный вид типа. Их, естественно, тоже можно будет описать.

Здравствуйте, D. Mon, Вы писали:

DM>Здравствуйте, deniok, Вы писали:

D>>Почему неизвестно? Определение же доступно.

DM>Да, действительно. Вот вариант на Идрисе, ближе к обсуждавшемуся zip'у:
DM>

DM>myzip : (l : List a) -> (r : List a) -> length l = length r -> List (a,a)
DM>myzip [] [] _ = []
DM>myzip (x::xs) (y::ys) e = (x,y) :: myzip xs ys (cong {f = pred} e)

DM>lenZip : (l : List a) -> (r : List a) -> (e: length l = length r) ->  length (myzip l r e) = length l
DM>lenZip [] [] _ = refl
DM>lenZip (x::xs) (y::ys) e = cong $ lenZip xs ys (cong e)
DM>

А кстати, то что тут нет необходимости в описании ещё двух случаев ((x::xs) [] и наоборот) — это следствие умного coverage checker'а Идриса или допустимости в нём частичных функций?

VD>>>В нем типы можно будет определять самостоятельно. В такие типы можно будет вносить все что душа пожелает.
CAB>>В чём отличие от создания классов?
VD>Класс – это конкретный вид типа. Их, естественно, тоже можно будет описать.
VD>Разницу между добавлением в язык классов и созданием конкретного класса представляешь? Вот это она и есть.
Класс, ИМХО, это наиболее общий тип, который может быть специализирован(не без костылей, но это проблемы реализации), к конкретному типу или виду типов.
VD>Мы делаем мета-сисстему.
Т.е. вы хотите спрятать код специализации типов в транслятор? Или у вас не будет типов(супертипов) вообще?
Например ФВП в ООП погут быть представлены как класс с одним методом:

  class Foo{
    def foo...
  }

А как описать ФВП в Н2?

Здравствуйте, deniok, Вы писали:

D>А кстати, то что тут нет необходимости в описании ещё двух случаев ((x::xs) [] и наоборот) — это следствие умного coverage checker'а Идриса или допустимости в нём частичных функций?

Я надеялся на первое, но оказалось второе. Вот с проверкой тотальности:

import Decidable.Equality

total
myzip : (l : List a) -> (r : List a) -> length l = length r -> List (a,a)
myzip [] [] _ = []
myzip [] (y::ys) _ = []
myzip (x::xs) [] _ = []
myzip (x::xs) (y::ys) e = (x,y) :: myzip xs ys (cong {f = pred} e)

total
lenZip : (l : List a) -> (r : List a) -> (e: length l = length r) ->
         length (myzip l r e) = length l
lenZip [] [] _ = refl
lenZip [] (y::ys) e = FalseElim $ OnotS e
lenZip (x::xs) [] e = FalseElim $ OnotS $ sym e
lenZip (x::xs) (y::ys) e = cong $ lenZip xs ys (cong e)

где (в стандартной библиотеке)

FalseElim : _|_ -> a
OnotS : O = S n -> _|_
sym : {l:a} -> {r:a} -> l = r -> r = l

Здравствуйте, D. Mon, Вы писали:

DM>Я надеялся на первое, но оказалось второе.

То есть, как я понимаю, в Идрисе за тотальностью при доказательствах нужно следить самостоятельно, выставляя модификатор total?

Здравствуйте, deniok, Вы писали:

D>То есть, как я понимаю, в Идрисе за тотальностью при доказательствах нужно следить самостоятельно, выставляя модификатор total?

Там есть выбор. Можно отдельные функции помечать словом total, можно в начале файла написать %default total, тогда все функции в файле будут проверяться на тотальность, а можно компилятору в командной строке дать ключик --total, тогда он будет вообще все проверять. Но если нигде ничего такого не сказать, то по умолчанию частичные функции допустимы, чтобы можно было писать как на обычном ФЯП.