Idris 1.3.3 Unexpected 'i'

@Bratjuuc · Регистрация: 12.08.2019

Студворк — интернет-сервис помощи студентам

Решил поставить Idris и начать пробовать писать простые вещи, но уже тут столкнулся с проблемой. Компилятор жалуется на простейшие воплощения инстансов классов, причём не на их содержание, а на кодовое слово "implementation".

Код

Кликните здесь для просмотра всего текста

Haskell
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
module Grid
import Matrix
 
data Input = X | O
 
size : Nat
size = 3
 
implementation Show Input
    show X = "X"
    show O = "O"
 
implementation Eq Input
    X == X = True
    O == O = True
    _ == _ = False
 
grid : Type
grid = matrix size size (Maybe Input)
 
rows :: List (Vector size (Maybe Input))
rows = ?hole

Компилятор выдаёт следующее:

Кликните здесь для просмотра всего текста

Haskell
1
2
3
4
5
6
7
Type checking .\Grid.idr
Grid.idr:9:1:
  |
9 | implementation Show Input
  | ^
unexpected 'i'
expecting "->", "<==", ';', end of input, or where block

По всем законам здравого смысла, того же Haskell, у меня всё написано правильно, я такое на Хаскелле 1000 раз делал. В чём может быть ошибка?

@Curry · 19.09.2024, 15:08

Я идрис особо не смотрел, но, там кажется, как и в haskell,

Haskell
1
instance Show Input where

К тому же, у вас в 21 строке двойное двоеточие, а это уже не haskell.

@Bratjuuc · 19.09.2024, 15:23 **[ТС]**

Слово

Haskell
1
instance

Можно использовать на Идрисе, но компилятор советует этого не делать, т.к. оно существует в Идрисе, чтобы облегчить жизнь хаскеллистам. У меня есть модуль Matrix, где все инстансы записаны через слово

Haskell
1
implementation

(правда мне пришлось скрыть инстанс моноида, т.к. компилятор на него жалуется той же ошибкой, что и в шапке темы).

Исправив двойное двоеточие на одинарное в 21 строчке и заменив implementation на instance, особо ничего не поменялось, т.к. она идёт после проблемной 9 строчки.

Кликните здесь для просмотра всего текста

Haskell
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
module Grid
import Matrix
 
data Input = X | O
 
size : Nat
size = 3
 
instance Show Input
    show X = "X"
    show O = "O"
 
implementation Eq Input
    X == X = True
    O == O = True
    _ == _ = False
 
grid : Type
grid = matrix size size (Maybe Input)
 
rows : List (Vector size (Maybe Input))
rows = ?hole

Кликните здесь для просмотра всего текста

Haskell
1
2
3
4
5
6
7
Type checking .\Grid.idr
Grid.idr:9:1:
  |
9 | instance Show Input
  | ^
unexpected 'i'
expecting "->", "<==", ';', end of input, or where block

@Curry · 19.09.2024, 16:11

Так работает

Haskell
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
data Input = X | O
 
size : Nat
size = 3
 
implementation Show Input where
    show X = "X"
    show O = "O"
 
implementation Eq Input where
    X == X = True
    O == O = True
    _ == _ = False
 
main : IO ()
main = print X

@extrn · 20.09.2024, 02:48

implementation тоже необязательно. просто

Haskell
1
2
3
Show Input where
  show X = "X"
  show O = "O"

А вместо class, если что - interface.
Вообще, языки отличаются значительно: и синтаксисом, и особенно системой типов.
Полагаться только на знание Haskell вряд ли получится.

XRuZzz · 28.12.2024, 08:41

Так уже Idris 2 давно вышел, 1 уже устарел.

@extrn · 30.12.2024, 22:53

Idris 2 очень крутой язык, прямо на порядок мощнее Idris. Вот только компилятор нестабильный пока до жути.
Чего стоит хотя бы вот это (обновлял экспериментальную версию несколько месяцев назад, так что м.б. уже пофиксили, но так-то и самому багу и баг-репорту соответственному - годы)

Haskell
1
2
3
total
absurdProof: 2 + 2 = 5
absurdProof = case () of False impossible

Первый обоснованно возразит, что с типами ты чего-то напутал, второй проглотит молча.
Это не позволяет лично мне им пользоваться для доказательств, т.к. тупо могу опечататься, и случайно доказать какую-нибудь чушь, а компилятор только кивнет.

Ну и пока даже до инструментария встроенного в компилятор первого, второму очень далеко. В общем когда-нибудь будет все круто, и первый уйдет на заслуженный покой, но пока оба нужны в арсенале.

Новые блоги и статьи Все статьи Все блоги /
SDL3 для Desktop (MinGW): Рисуем цветные прямоугольники с помощью рисовальщика SDL3 на Си и C++ 8Observer8 17.03.2026 Содержание блога Финальные проекты на Си и на C++: finish-rectangles-sdl3-c. zip finish-rectangles-sdl3-cpp. zip	Символические и жёсткие ссылки в Linux. algri14 15.03.2026 Существует два типа ссылок — символические и жёсткие. Ссылка в Linux — это запись в каталоге, которая может указывать либо на inode «файла-ИСТОЧНИКА», тогда это будет «жёсткая ссылка» (hard link),. . .	[Owen Logic] Поддержание уровня воды в резервуаре количеством включённых насосов: моделирование и выбор регулятора ФедосеевПавел 14.03.2026 Поддержание уровня воды в резервуаре количеством включённых насосов: моделирование и выбор регулятора ВВЕДЕНИЕ Выполняя задание на управление насосной группой заполнения резервуара,. . .	делаю науч статью по влиянию грибов на сукцессию anaschu 13.03.2026 прикрепляю статью
SDL3 для Desktop (MinGW): Создаём пустое окно с нуля для 2D-графики на SDL3, Си и C++ 8Observer8 10.03.2026 Содержание блога Финальные проекты на Си и на C++: hello-sdl3-c. zip hello-sdl3-cpp. zip Результат:	Установка CMake и MinGW 13.1 для сборки С и C++ приложений из консоли и из Qt Creator в EXE 8Observer8 10.03.2026 Содержание блога MinGW - это коллекция инструментов для сборки приложений в EXE. CMake - это система сборки приложений. Здесь описаны базовые шаги для старта программирования с помощью CMake и. . .	Как дизайн сайта влияет на конверсию: 7 решений, которые реально повышают заявки Neotwalker 08.03.2026 Многие до сих пор воспринимают дизайн сайта как “красивую оболочку”. На практике всё иначе: дизайн напрямую влияет на то, оставит человек заявку или уйдёт через несколько секунд. Даже если у вас. . .	Модульная разработка через nuget packages DevAlt 07.03.2026 Сложившийся в . Net-среде способ разработки чаще всего предполагает монорепозиторий в котором находятся все исходники. При создании нового решения, мы просто добавляем нужные проекты и имеем. . .

XRuZzz Антикодер 1888 / 870 / 48 Регистрация: 15.09.2012 Сообщений: 3,088
	28.12.2024, 08:41
	Так уже Idris 2 давно вышел, 1 уже устарел. 1