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

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

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

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

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

РЕДАКТИРОВАТЬ: как упоминал dfeuer, контексты Datatype не являются хорошей идеей. Я могу провести сравнение на уровне значений, но я хочу иметь возможность делать это на уровне типа:

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)))

~~~~

РЕДАКТИРОВАТЬ: Sorta ответила на мой собственный вопрос, просто добавив ограничение к экземпляру:

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


haskell type-level-computation dependent-type
person Aistis Raulinaitis    schedule 13.01.2016    source источник
comment
Это контекст типа данных. Контексты типов данных совершенно бесполезны. Я подозреваю, что вы пока не сможете делать именно то, что пытаетесь сделать в Haskell, но синглтоны могут делать некоторые странные вещи ...   -  person dfeuer    schedule 13.01.2016
comment
Да, вы правы, контексты типов данных - это не совсем то, что я хотел бы сделать. Но они понимают суть. Я могу переопределить значение типа и провести сравнение на уровне значения, но это не то, что я хочу делать.   -  person Aistis Raulinaitis    schedule 13.01.2016
comment
Не могли бы вы немного лучше объяснить, в чем именно заключается ваша конечная цель? Что вы действительно хотите выразить?   -  person dfeuer    schedule 13.01.2016
comment
Я просто хочу иметь возможность взять nat уровня типа и список уровней типа и проверить, что n ~ Length ls на уровне типа, я не хочу делать это на уровне значения. Я отредактировал свой OP с дополнительными деталями.   -  person Aistis Raulinaitis    schedule 13.01.2016
comment
Вы видели такие пугающие вещи, как Data.Singletons.Prelude.Eq? Я не знаю, что с этим делать, но вполне может быть способ попроще.   -  person dfeuer    schedule 13.01.2016

Ответы (2)


arrow_upward
4
arrow_downward

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

{-# 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.

person user2407038    schedule 13.01.2016
comment
Отлично, это довольно близко к тому, что я ищу! Хотя, как мне заставить это работать с прокси? - person Aistis Raulinaitis; 13.01.2016
comment
Да, я хочу носить с собой этот инвариант. Но я не хочу определять отдельный TList, он должен использовать прокси. - person Aistis Raulinaitis; 13.01.2016
comment
Невозможно - вся суть Proxy в том, что он не несет информации о типе. Я не понимаю, зачем вам конкретно нужно использовать прокси - вы всегда можете создать Proxy. Конечно, вы можете просто разместить ограничение там, где оно вам нужно, и использовать там Proxy: Length xs ~ n => Proxy xs -> Proxy n -> ..., но тогда у вас нет правильного свойства по конструкции. - person user2407038; 14.01.2016
comment
Ха, правда, мне кажется, что прокси - это полная противоположность тому, что вы сказали, он не несет данных, он предназначен только для хранения типов. Хотя мог совершенно ошибаться. - person Aistis Raulinaitis; 16.01.2016
comment
Proxy :: Proxy x изоморфен () во время выполнения для любого типа x. Он не хранит тип x ни в каком качестве. Это не относится к TList. Во время выполнения ограничения становятся конкретными значениями, поэтому тип TList, по сути, TList :: Coercion (Length xs) n -> TList n xs - Coercion - это внутренний тип, используемый GHC для представления равенств типов - он является свидетелем равенства двух типов во время выполнения, следовательно, информация о типе во время выполнения. - person user2407038; 16.01.2016
comment
Спасибо! В этом есть смысл! - person Aistis Raulinaitis; 16.01.2016
comment
Вы можете импортировать Data.Type.Equality, чтобы получить :~:, вместо того, чтобы определять его самостоятельно. - person dfeuer; 11.12.2016

arrow_upward
3
arrow_downward

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

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 работает в библиотеке синглтонов, но полагаю, что вы могли бы сделать что-то подобное.

person dfeuer    schedule 13.01.2016
comment
Хороший пример, но я хочу использовать nats встроенного типа GHC. Плюс я ответил на свой вопрос! - person Aistis Raulinaitis; 13.01.2016