История изменений
Исправление quasimoto, (текущая версия) :
В чем вы видите разницу?
Я согласился, что разницы нет (в той же агде 5 это сахар для таких sss...), тут дело в другом - я там написал достаточно. Это обычная логика - с S S S S S Z : Nat нам есть что делать, с q : S S S S S Z - нечего, мы толком не знаем что это (разве что написать id : 5 -> 5; id x = x), можно считать, что 5 это точка типа (множества) Nat, которая сама по себе не множество.
Это не сумма, а объединение.
Ну or это и есть сумма типов, на уровне термов сумма = объединение (тегированное, если что).
Проблема в следующем - как задать произвольную функциональную зависимость?
Так же как в типе обычной функции.
Напишите тип для yoba.
Причём это не top-level определение? Так как никакого define нет, есть let - yoba x body = ⟦ let $ x = 1 in $ body ⟧; yoba : {T : Set} → ⟪ Name Int ⟫ → ⟪ T ⟫ → ⟪ T ⟫ (или ⟪ Name Int ⟫ → ⟪ Expr T ⟫ → ⟪ Expr T ⟫).
Ну где реализация-то?
Там нужно дописать что-то вроде
class HFlatten tree l | tree -> l where hFlatten :: tree -> l
instance HFlatten HNil HNil where hFlatten _ = HNil
instance HFlatten (HBox t) (HBox t) where hFlatten = id
instance (HFlatten t l, Flatten t' l', HAppend l l' l'') => HFlatten (t, t') l'' where flatten (l, r) = hAppend (flatten l) (flatten r)
но использовать всё равно невозможно (как и всю hlist) - типы не выводятся.
Есть такой flatten, можно либо так:
data MyData = MyInteger Integer | MyString String | ...
myFlatten :: Tree MyData -> [MyData]
myFlatten = flatten
либо так:
myFlatten :: Tree Dynamic -> [Dynamic]
myFlatten = flatten
Я не знаю какое у вас определение программы. Для меня программа - это терм ЯП. Разные термы - разные программы.
Для меня программа это нечто что кроме своей функциональности (набора функций работающих с данными таких-то типов) имеет ещё как минимум _интерфейс_. Число 5 - терм языка, но явно не программа (хотя его можно его превратить в программу суть которой в печатании числа «5», показывании «<html><head>...</head><body>5</body></html>», отправлении слова 5 по сети по такому-то протоколу и т.п. - нужно добавить соответствующий интерфейс).
Да.
Ну например (app f pat) применяет любую функцию f и матчит относительно паттерна pat.
fun :: [T] -> ...
fun [] = ... -- PM
fun [x] | pred x = ... -- PM + Guards
| ...
fun (x:y:zs) | x > n, pat <- x, y < m, pat <- y, ... = ... -- PM + Guards + PM + Guards + PM + ...
| pat <- act zs, ... -- Action PM + ...
Речь шла о том, какая практическая польза от обсуждаемой системы метапрограммирования?
Ну, а какая польза от N2? Там тоже предполагается ограничивать макросы правилами типизации.
Исходная версия quasimoto, :
В чем вы видите разницу?
Я согласился, что разницы нет (в той же агде 5 это сахар для таких sss...), тут дело в другом - я там написал достаточно. Это обычная логика - с S S S S S Z : Nat нам есть что делать, с q : S S S S S Z - нечего, мы толком не знаем что это (разве что написать id : 5 -> 5; id x = x), можно считать, что 5 это точка типа (множества) Nat, которая сама по себе не множество.
Это не сумма, а объединение.
Ну or это и есть сумма типов, на уровне термов сумма = объединение (тегированное, если что).
Проблема в следующем - как задать произвольную функциональную зависимость?
Так же как в типе обычной функции.
Напишите тип для yoba.
Причём это не top-level определение? Так как никакого define нет, есть let - yoba x body = ⟦ let $ x = 1 in $ body ⟧; yoba : {T : Set} → ⟪ Name Int ⟫ → ⟪ T ⟫ → ⟪ T ⟫ (или ⟪ Name Int ⟫ → ⟪ Expr T ⟫ → ⟪ Expr T ⟫).
Ну где реализация-то?
Там нужно дописать что-то вроде
class HFlatten tree l | tree -> l where hFlatten :: tree -> l
instance HFlatten HNil HNil where hFlatten _ = HNil
instance HFlatten (HBox t) (HBox t) where hFlatten = id
instance (HFlatten t l, Flatten t' l', HAppend l l' l'') => HFlatten (t, t') l'' where flatten (l, r) = hAppend (flatten l) (flatten r)
но использовать всё равно невозможно (как и всю hlist) - типы не выводятся.
Есть такой flatten, можно либо так:
data MyData = MyInteger Integer | MyString String | ...
myFlatten :: Tree MyData -> [MyData]
myFlatten = flatten
либо так:
myFlatten :: Tree Dynamic -> [Dynamic]
myFlatten = flatten
Я не знаю какое у вас определение программы. Для меня программа - это терм ЯП. Разные термы - разные программы.
Для меня программа это нечто что кроме своей функциональности (набора функций работающих с данными таких-то типов) имеет ещё как минимум _интерфейс_. Число 5 - терм языка, но явно не программа (хотя его можно его превратить в программу суть которой в печатании числа «5», показывании «<html><head>5</head></html>», отправлении слова 5 по сети по такому-то протоколу и т.п. - нужно добавить соответствующий интерфейс).
Да.
Ну например (app f pat) применяет любую функцию f и матчит относительно паттерна pat.
fun :: [T] -> ...
fun [] = ... -- PM
fun [x] | pred x = ... -- PM + Guards
| ...
fun (x:y:zs) | x > n, pat <- x, y < m, pat <- y, ... = ... -- PM + Guards + PM + Guards + PM + ...
| pat <- act zs, ... -- Action PM + ...
Речь шла о том, какая практическая польза от обсуждаемой системы метапрограммирования?
Ну, а какая польза от N2? Там тоже предполагается ограничивать макросы правилами типизации.