Purescript рассматривает класс как синоним циклического типа - PullRequest
Новая
       7

Purescript рассматривает класс как синоним циклического типа

0 голосов
/ 12 мая 2019

Я пытаюсь определить экземпляры, которые работают только с натуральными числами уровня типа.Когда я компилирую этот файл: 

module Main where

data NatZero
data NatSucc n

class NatClass n where
   switch :: f NatZero -> (forall m. NatClass m => f (NatSucc m)) -> f n

, он говорит мне: 

Error found:
at src/Main.purs:6:1 - 7:73 (line 6, column 1 - line 7, column 73)

  A cycle appears in the definition of type synonym NatClass
  Cycles are disallowed because they can lead to loops in the type checker.
  Consider using a 'newtype' instead.

Почему NatClass стал синонимом типа?Я думал, что это был типовой класс.И где там петля?Что я должен изменить, чтобы сделать эту работу, как в Haskell?Это говорит мне о новом типе, что я нового типа?

1 Ответ

2 голосов
/ 12 мая 2019

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

В настоящее время словарь представлен как запись, поэтому синоним, упомянутый в ошибке здесь, заключается в том, что компилятор создает что-то подобное для класса: 

type NatClass n = 
  { switch :: forall f. f NatZero -> (forall m. NatClass m => f (NatSucc m)) -> f n }

Так что он может выполнять довольно прямую замену ограничений на словарные аргументы.

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

Я давно хотел изменить представление для классов типов, и у меня есть WIP PR , я думаю, что после этого подобные вещи будут разрешены. После этого классы будут десагарации в тип data, а не в синоним, поэтому ссылка должна быть разрешена.

...