Я надеюсь, что некоторые эксперты 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
но это не то, что мне нужно.
Спасибо!
Ранджит.