Ограничения равенства для списков уровней типов

Question

Я пытаюсь применить ограничение уровня типа, чтобы список типов типов был такой же длины, что и нагрузка типа Nat. Например, при использовании Длины от Singletons [1] пакета:

data (n ~ Length ls) => NumList (n :: Nat) (ls :: [*]) 

test :: Proxy (NumList 2 '[Bool, String, Int]) 
test = Proxy 

Я бы не ожидал этот код для компиляции, поскольку существует несоответствие.

EDIT: Как упоминалось в dfeuer Контексты типа данных - это не очень хорошая идея. Я могу сделать сравнение на уровне значения, но я хочу, чтобы быть в состоянии сделать это на уровне типа:

class NumListLen a 
    sameLen :: Proxy a -> Bool 

instance (KnownNat n, KnownNat (Length m)) => NumListLen (NumList n m) where 
    sameLen = const $ (natVal (Proxy :: Proxy n)) == (natVal (Proxy :: Proxy (Length m))) 

~~~~

EDIT: Сорт ответил на свой вопрос, просто добавьте ограничением для экземпляра:

class NumListLen a 
    sameLen :: Proxy a -> Bool 

instance (KnownNat n, KnownNat (Length m), n ~ Length m) => NumListLen (NumList n m) where 
    sameLen = const $ (natVal (Proxy :: Proxy n)) == (natVal (Proxy :: Proxy (Length m))) 

/home/aistis/Projects/SingTest/SingTest/app/Main.hs:333:13: 
    Couldn't match type ‘3’ with ‘2’ 
    In the second argument of ‘($)’, namely ‘sameLen test’ 
    In a stmt of a 'do' block: print $ sameLen test 
    In the expression: 
     do { print $ sameLen test; 
      putStrLn "done!" } 

[1] https://hackage.haskell.org/package/singletons-2.0.0.2/docs/Data-Promotion-Prelude-List.html#t:Length

Answer 1

Одним из вариантов может быть для использования семейства типов:

data Nat = Z | S Nat 

type family LengthIs (n :: Nat) (xs :: [*]) :: Bool where 
    LengthIs 'Z '[] = 'True 
    LengthIs ('S n) (x ': xs) = LengthIs n xs 
    LengthIs n xs = 'False 

test :: LengthIs ('S ('S 'Z)) '[Bool,String,Int] ~ 'True =>() 
test =() 

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

Answer 2

Если это что-то вроде инварианта (который, кажется, что это), вы должны хранить доказательства в тип данных:

{-# LANGUAGE PolyKinds, UndecidableInstances #-} 

import GHC.TypeLits 

type family Length (xs :: [k]) :: Nat where 
    Length '[] = 0 
    Length (x ': xs) = 1 + Length xs 

data TList n l where 
    TList :: (Length xs ~ n) => TList n xs 

Обратите внимание, что в то время как доказательство по-прежнему доступен на уровне типа, то вроде «скрытого» за конструктором данных. Вы можете восстановить доказательство просто сопоставление с образцом:

data (:~:) a b where Refl :: a :~: a 

test :: TList n l -> Length l :~: n 
test TList = Refl 

Теперь несоответствием между двумя параметрами являются ошибками типа:

bad :: TList 3 '[Int, Bool] 
bad = TList 

good :: TList 2 '[Int, Bool] 
good = TList 

Конечно, это все еще может быть побежден донными значениями, так

uh_oh :: TList 10 '[] 
uh_oh = undefined 

Чтобы избежать этого, просто убедитесь, что вы всегда сопоставляете шаблон по конструктору TList.