Инструменты Digitable
Архитектор
Слева холст, справа модель на языке. Нарисованное превращается в объявления теорката и тут же проверяется компилятором — тем самым, что стоит за flang check. Написанное раскладывается обратно в фигуры.
Что на холсте чем становится
| На холсте | В языке | Что проверяет компилятор |
|---|---|---|
| Рамка с подписью | объект «Имя» | имя не занято другим объектом |
| Сплошная стрелка с подписью | морфизм «Имя» из «А» в «Б» | оба конца объявлены объектами |
| Петля на рамке | единица «А» | объект объявлен |
| Пунктирная стрелка | морфизм «Имя» это «г» после «ф» | кодомен первой стрелки совпал с доменом второй |
Пунктир выбран не по вкусу: в коммутативных диаграммах им рисуют выведенную стрелку — ту, существование которой следует из остальных. Композиция и есть такая стрелка: отдельно она не рисуется, она получается из пути.
Холст и модель
Редактор весит около 430 КБ по сети и грузится только по этой кнопке.
Чего страница не делает
- Круги Эйлера не переводятся. Пересечению множеств в языке не соответствует ничего: равенство типов номинальное — по имени, — подтипов нет, а произведение (запись) и копроизведение (тип с вариантами) — это не пересечение и не объединение. Нарисовать два круга внахлёст можно, объявления из этого не выйдет.
- Изоморфизм по паре встречных стрелок не выводится. Пара стрелок туда и обратно изоморфизмом не является: изоморфизм утверждает, что их композиции равны единицам, и это допущение автора, а не свойство рисунка. Написать его в панели можно, компилятор проверит; вывести из картинки — нет.
- Подсветка работает в панели, а не на холсте. У текста внутри фигуры Excalidraw одно поле
textи один цветstrokeColorна весь элемент: места под разметку по кускам в формате нет, и рисуется он одним вызовомfillText. Раскрасить надпись внутри рамки нельзя, не переписав редактор.