LINUX.ORG.RU
Форум — Development  

Не выводится констрейнт! Памагите

 , ,


0

2 
> {-# LANGUAGE DataKinds, TypeOperators, KindSignatures, GADTs, ConstraintKinds, TypeFamilies, UndecidableInstances #-}
> 
> import GHC.TypeLits
> import Data.Constraint
> import Data.Proxy

> data Proof2 :: (Nat -> Constraint) -> * where
>   Proof2 :: c n => Proxy n -> Proof2 c
>
> type family LessThen255 n :: Constraint where
>     LessThen255 f = (f <= 255)
>
> one :: LessThen255 n => Proxy n -> Proof2 LessThen255
> one = Proof2

Выдает очень неожиданное

Min.lhs:14:9:
    Could not deduce (LessThen255 n) arising from a use of ‘Proof2’
    from the context (LessThen255 n)
      bound by the type signature for
                 one :: (LessThen255 n) => Proxy n -> Proof2 LessThen255

куда копать?

P.S. изменение на

> data Proof2 :: (Nat -> Constraint) -> Nat -> * where
>   Proof2 :: c n => Proxy n -> Proof2 c n

(избавились от экзистенциализма) не помогает

★★★★★

Последнее исправление: qnikst (всего исправлений: 2)
← Как на Java сказать «Hello, world!» ?
Не запускается Emacs code browser в Emacs24 →

Не в тему, но сколько я не пытался работать в хаскелле с «зависимыми типами», получалось честно говоря не очень. В кавычках, потому что зависимых типов в хаскелле как таковых нет.

hateyoufeel ★★★★★
()
Последнее исправление: hateyoufeel (всего исправлений: 1)
Ответ на: комментарий от hateyoufeel

Ну почему же уже в 7.8 все стало гораздо приличнее, и typelevel literals и typelevel naturals и синглтонами, но все равно конечно не агда.

qnikst ★★★★★
() автор топика
Ответ на: комментарий от qnikst

Ну почему же уже в 7.8 все стало гораздо приличнее, и typelevel literals и typelevel naturals и синглтонами, но все равно конечно не агда.

Я скорее на Idris в этом плане поглядываю.

hateyoufeel ★★★★★
()

Вот так вроде работает:

one :: forall c n. (LessThen255 ~ c, c n) => Proxy n -> Proof2 c                                                                        one = Proof2

Почему - хз. Вероятно, бага в GHC.

anonymous
()
Ответ на: комментарий от anonymous

да 

> one :: (LessThen255 ~ c, c n) => Proxy n -> Proof2 c
> one = Proof2

сработало, спасибо.

qnikst ★★★★★
() автор топика

7.8.2 выдаёт вот что: 

    Type synonym ‘LessThen255’ should have 1 argument, but has been given none
    In the type signature for ‘one’:
      one :: LessThen255 n => Proxy n -> Proof2 LessThen255

Miguel ★★★★★
()
Ответ на: комментарий от Miguel

есть дистрибутивы, где все ещё используется 7.8.2? он же баги в работе с семействами типов имеет..

Тут все нормально, у LessThen255 kind Nat -> Constraint, т.е. LessThen255 n - Constraint, все верно, а в Proof2 у аргумента типа Kind должен быть Nat -> Constraint, что и есть.

qnikst ★★★★★
() автор топика
Ответ на: комментарий от Miguel

на рабочей машинке 7.8.3, сейчас буду готовить контейнер с HEAD.

на старой рабочей 7.6.последнее и 7.8.3.

qnikst ★★★★★
() автор топика
Ответ на: комментарий от Miguel

опять же это тут ни при чем, скорее всего просто баг, т.к. в общем-то идентичный код Не выводится констрейнт! Памагите (комментарий) тут работает.

Я вот HEAD щас ещё попробую..

UPD не попробую под него надо constraints соберать, а мне лень.

qnikst ★★★★★
() автор топика
Последнее исправление: qnikst (всего исправлений: 2)
Ответ на: комментарий от qnikst

Короче, всё как всегда: с данными проще работать, чем с классами: 

{-# LANGUAGE DataKinds, TypeOperators, GADTs, KindSignatures #-}
module Main where
import GHC.TypeLits
import Data.Proxy
data LessThen255 n where LessThen255 :: (n <= 255) => LessThen255 n
data Proof2 :: (Nat -> *) -> * where Proof2 :: c n -> Proxy n -> Proof2 c
one :: LessThen255 n -> Proxy n -> Proof2 LessThen255
one = Proof2

Miguel ★★★★★
()
Последнее исправление: Miguel (всего исправлений: 1)
Ответ на: комментарий от Miguel

если бы так ещё словари KnownNat, потаскать можно было, хотя ведь с помощью Dict можно?

qnikst ★★★★★
() автор топика
Ответ на: комментарий от Miguel 

> guessProof :: (KnownNat n, n <= 255) => SomeNat -> Proxy n -> Maybe (Proof2D LessThen255D)
> guessProof (SomeNat p) n = case sameNat p n of
>     Just _  -> Just $ Proof2D (c2dk n) LessThen255D n
>     Nothing -> Nothing

> type family Guesses (n::Nat) :: [Nat] where
>    Guesses 0 = '[0]
>    Guesses n = n ': Guesses (n-1)


> g :: Proxy n -> Proxy (Guesses n)
> g _ = Proxy

> class GuessProof (n :: [Nat]) where
>   proof :: SomeNat -> Proxy n -> Maybe (Proof2D LessThen255D)


> instance GuessProof '[] where
>   proof _ _ = Nothing

> instance (KnownNat n, n <= 255) => GuessProof (n ': ns) where
>   proof s p = guessProof s (inner p)
>    where inner :: Proxy (n ': ns) -> Proxy (n::Nat)
>          inner _ = Proxy

оно даже работает с горем пополам, но блин проще использовать свои числа, чем Num.

P.S. естественно в реальном коде это нафиг не надо.

qnikst ★★★★★
() автор топика
Последнее исправление: qnikst (всего исправлений: 1)
Ответ на: комментарий от qnikst

поправка.

> instance (KnownNat n, n <= 255, GuessProof ns) => GuessProof (n ': ns) where
>   proof s p = case guessProof s (inner p) of
>                 Nothing -> proof s (next p)
>                 x -> x
>    where inner :: Proxy (n ': ns) -> Proxy (n::Nat)
>          inner _ = Proxy
>          next :: Proxy (n ': ns) -> Proxy (ns::[Nat])
>          next _ = Proxy
qnikst ★★★★★
() автор топика
Ответ на: комментарий от Miguel

Если ещё будут идеи, как использовать с этим KnowNat - пиши, а то смотри:

> data Proof2D :: (Nat -> *) -> * where
>   Proof2D :: Dict (KnownNat n) -> c n -> Proxy n -> Proof2D c

> instance Show (Proof2D c) where
>   show (Proof2D _ _ k) = show (natVal k)

Min.lhs:22:34:
    No instance for (KnownNat n) arising from a use of ‘natVal’
    Possible fix:
      add (KnownNat n) to the context of
        the data constructor ‘Proof2D’
        or the instance declaration

это поидее через reflection может решиться, но я его не умею :/

qnikst ★★★★★
() автор топика
Последнее исправление: qnikst (всего исправлений: 1)
Ответ на: комментарий от qnikst

А вообще Кметт — это такое l'enfant terrible. В частности я почти уверен, что всё будет лучше, если использовать вместо Dict вот такое: 

data Dictionary c a where Dictionary :: c a => Dictionary c a
data Proof2D :: (Nat -> *) -> * where
  Proof2D :: Dictionary KnownNat n -> c n -> Proxy n -> Proof2D c

Miguel ★★★★★
()
Ответ на: комментарий от Miguel

сама задача попытаться засунуть юзерское число в часть программы где есть constraint (n <= 255).

По мотивам: https://www.haskell.org/pipermail/glasgow-haskell-users/2014-November/025451....

При этом хочется минимально читерить и сохранить максимум свойств, которые можно иметь.

То, что выше, это просто хочется иметь аналог SomeNat, то только с каким-нибудь дополнительным constraint-ом и уметь такие штуки адекватно создавать.

qnikst ★★★★★
() автор топика
Ответ на: комментарий от tailgunner

void for_1_10(void (*f)());

постигни суть борща

anonymous
()
Ответ на: комментарий от qnikst

тогда вернёмся к предыдущим проблемам, где из KnownNat не следует KnownNat.

Да вроде нет, я попробовал в FPComplete и оно скомпилировалось.

Код: 

> {-# LANGUAGE DataKinds, TypeOperators, GADTs, TypeFamilies, UndecidableInstances #-}
> import Control.Applicative
> import Control.Monad
> import GHC.TypeLits
> import Data.Proxy
> data Proof2D :: (Nat -> *) -> * where Proof2D :: KnownNat n => (Proxy n -> Integer) -> c n -> Proxy n -> Proof2D c
> instance Show (Proof2D c) where show (Proof2D _ _ k) = show $ natVal k
> data LessThen255D (n::Nat) where LessThen255D :: (n <= 255) => LessThen255D n
> oned :: KnownNat n => (Proxy n -> Integer) -> LessThen255D n -> Proxy n -> Proof2D LessThen255D
> oned = Proof2D
> c2dk :: KnownNat n => Proxy n -> (Proxy n -> Integer) -- Dict (KnownNat n)
> c2dk _ = natVal 
> guessProof :: (KnownNat n, n <= 255) => SomeNat -> Proxy n -> Maybe (Proof2D LessThen255D)
> guessProof (SomeNat p) n = Proof2D (c2dk n) LessThen255D n <$ sameNat p n
> data N = Z | S N
> type family Guesses (n::Nat) :: [Nat] where
>    Guesses 0 = '[0]
>    Guesses n = n ': Guesses (n-1)
> g :: Proxy n -> Proxy (Guesses n)
> g _ = Proxy
> class GuessProof (n :: [Nat]) where proof :: SomeNat -> Proxy n -> Maybe (Proof2D LessThen255D)
> instance GuessProof '[] where proof _ _ = Nothing
> instance (KnownNat n, n <= 255, GuessProof ns) => GuessProof (n ': ns) where
>   proof s p = guessProof s (inner p) `mplus` proof s (next p)
>    where inner :: Proxy (n ': ns) -> Proxy (n::Nat)
>          inner _ = Proxy
>          next :: Proxy (n ': ns) -> Proxy (ns::[Nat])
>          next _ = Proxy
> main :: IO()
> main = return ()
> type family C2N (n::N) :: Nat where
>   C2N 'Z = 0
>   C2N ('S x) = 1 + C2N x

Miguel ★★★★★
()
Последнее исправление: Miguel (всего исправлений: 1)
Ответ на: комментарий от Miguel

да, верно, но с KnownNat была какая-то проблема, что оно не доказывалось, возможно с чем-то другим связанная..

qnikst ★★★★★
() автор топика
Ответ на: комментарий от Miguel

к слову, я должен извиниться про 7.8.2, на самом деле баг именно в 7.8.3

Вот что написал Ричард Эйзенберг:

By the way, the bug in the Proof2 version is a bug in GHC 7.8.3 (only in .3 — not in .2 or in the soon-to-be .4) that allows you to write unsaturated type families that don't work. Saying `LessThan255` without a parameter should be a syntax error, but that check was accidentally turned off for 7.8.3, leading to a bogus type error.

qnikst ★★★★★
() автор топика
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.
← Как на Java сказать «Hello, world!» ?
Development
Не запускается Emacs code browser в Emacs24 →