Кодировка "Меньше чем" с Haskell

Я надеюсь, что некоторые эксперты Haskell могут помочь прояснить ситуацию.

Можно ли определить Nat обычным способом (через @dorchard Singleton types в Haskell)

data S n = Succ n 
data Z   = Zero

class Nat n 
instance Nat Z
instance Nat n => Nat (S n)

(или его вариант), а затем определить отношение LessThan такой, что forall n и m

LessThan Z (S Z)
LessThan n m => LessThan n     (S m)
LessThan n m => LessThan (S n) (S m)

а затем напишите функцию с типом типа:

foo :: exists n. (LessThan n m) => Nat m -> Nat n
foo (S n) = n
foo Z     = foo Z

Я явно хочу использовать "LessThan" в типе вывода для foo, Я понимаю, что можно было бы написать что-то вроде

foo :: Nat (S n) -> Nat n

но это не то, что мне нужно.

Спасибо!

Ранджит.

Ответы

Ответ 1

Здесь один из способов реализовать что-то похожее на то, о чем вы просите.

Нат

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

data Z
data S n

data Nat n where
  Zero :: Nat Z
  Succ :: Nat n -> Nat (S n)

LessThan

Мы также можем определить LessThan как тип.

data LessThan n m where
  LT1 :: LessThan Z (S Z)
  LT2 :: LessThan n m -> LessThan n (S m)
  LT3 :: LessThan n m -> LessThan (S n) (S m)

Обратите внимание, что я просто добавил три свойства и превратил их в конструкторы данных. Идея этого типа состоит в том, что полностью нормированное значение типа LessThan n m является доказательством того, что n меньше m.

Работа для экзистенций

Теперь вы спрашиваете о:

foo :: exists n. (LessThan n m) => Nat m -> Nat n

Но в Хаскелле не существует. Вместо этого мы можем определить тип данных только для foo:

data Foo m where
  Foo :: Nat n -> LessThan n m -> Foo m

Обратите внимание, что здесь n фактически существует в количественном выражении, потому что оно появляется в аргументах конструктора данных foo, но не в его результате. Теперь мы можем указать тип foo:

foo :: Nat m -> Foo m

Лемма

Прежде чем мы сможем реализовать пример из вопроса, нам нужно доказать небольшую лемму о LessThan. Лемма говорит, что n меньше S n для всех n. Докажем это индукцией по n.

lemma :: Nat n -> LessThan n (S n)
lemma Zero = LT1
lemma (Succ n) = LT3 (lemma n)

Реализация foo

Теперь мы можем написать код из вопроса:

foo :: Nat m -> Foo m
foo (Succ n) = Foo n (lemma n)
foo Zero = foo Zero