Соответствие на уровне типа Nat в GHC 7.6

Мой вопрос, наверное, проще всего объяснить на примере:

type family   Take (n :: Nat) (xs :: [k]) :: [k]
type instance Take 0     xs        = '[]
type instance Take (n+1) (x ': xs) = x ': Take n xs

Однако второй экземпляр здесь отклоняется, потому что (+), сам являясь семейством типов, не может использоваться в аргументах. Но, похоже, нет ничего Succ или чего-то еще, что обычно используется для сопоставления Nats.

Итак, можно ли это выразить; и если да, то как?

Обновить. Я заметил, что функции isZero и isEven в GHC.TypeLits находятся под заголовком« Уничтожение типов ». Предназначены ли они как-то для использования на уровне типов? Я бы подозревал, что нет ... но в основном потому, что не знаю, как это сделать. :)


haskell type-level-computation ghc type-families
person Andy Morris    schedule 17.09.2012    source источник
comment
Верно. Я только что установил GHC 7.6, чтобы иметь возможность проверить этот код, и обе проблемы, о которых вы упоминаете в своих комментариях ниже, были отмечены GHC. Извинения. (Я нажал кнопку «Удалить» в своем ответе, поэтому теперь не могу комментировать его напрямую).   -  person macron    schedule 17.09.2012
comment
Похоже, кодирование условий завершения в качестве аргументов может работать (см. gist.github.com/a39ce17ca47798b0f0ef), но это только кажется успешным, когда n == 1. Я пробовал это на ветке type-nats, а не на 7.6, так что ymmv.   -  person Nathan Howell    schedule 18.09.2012
comment
Функции isZero и isEven создают одноименные GADT, которые предоставляют доступ к предикату уровня типа на уровне термина. Другими словами, это способ найти соответствие, которое вы хотите, в обычной функции на уровне термина, а не в функции типа. : [   -  person C. A. McCann    schedule 26.09.2012

Ответы (1)


arrow_upward
5
arrow_downward

Я думаю, что это известная проблема в текущей реализации TypeNats. Но над этим работают, посмотрите: https://plus.google.com/117760254622432568621/posts/iMYU2SMViay < / а>

person michalt    schedule 23.09.2012