← All posts tagged typefun

qnikst
? :( Haskell typefun type family LessThen255 n :: Constraint where
LessThen255 f = (f <= 255)

class KnownNat n => FindEq (c::Nat -> Constraint) (n::Nat) where
findEq :: (KnownNat p) => Proxy n -> Proxy p -> Maybe (Proof2 c)

instance FindEq LessThen255 0 where findEq = Nothing
а так, что нельзя чтоли?
qnikst
? Haskell typefun Вот есть у меня, например, Proxy (n::Nat), можно как-нибудь убедить компилятор, что оно удовлетворяет какому-нибудь ограничению, типа

data P where
P :: (n < 255) => Proxy n -> P

magick :: Proxy n -> Maybe P
magick = undefined


даже unsafeCoerce не спасает..
qnikst
:( Haskell typefun Proof.lhs:70:14:
Could not deduce (LessThen255 n) arising from a use of ‘magick’
from the context (LessThen255 n, KnownNat n)
bound by the type signature for
magicEx1 :: (LessThen255 n, KnownNat n) =>
Proxy n -> Proof2 LessThen255
at Proof.lhs:69:15-74
Relevant bindings include
magicEx1 :: Proxy n -> Proof2 LessThen255 (bound at Proof.lhs:70:3)
In the expression: magick Dict
In an equation for ‘magicEx1’: magicEx1 = magick Dict
qnikst
code Haskell typefun
Во какая доброта получилась, можно держать ядро программы
где требуется выполнение всяких требований и четко отделить его
от части программы где поступает вход от юзера, таким образом сразу видно, 
где и какие проверки требуются. Наверняка же ещё упростить можно?

> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE ScopedTypeVariables #-}
> {-# LANGUAGE KindSignatures #-}
> {-# LANGUAGE ExistentialQuantification #-}
> {-# LANGUAGE ViewPatterns #-}
> {-# LANGUAGE PolyKinds #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE UndecidableInstances #-}
>
> import GHC.TypeLits
> import GHC.Exts 
> import Data.Proxy
> import System.Environment


> data Proof n  (c :: Constraint) where Proof :: Proxy n -> Proof n c

And runtime converter that checks constraint at runtime:

> fromSome :: SomeNat -> Maybe (Proof n (n <= 255))
> fromSome (SomeNat p)
>    | natVal p <= 255 = Just (Proof (Proxy :: Proxy n))
>    | otherwise = Nothing

> main :: IO ()
> main = do
>     [arg] <- getArgs
>     let n = read arg :: Integer
>
>     case someNatVal n of
>       Nothing -> error "Input is not a natural number!"
>       Just sn -> case fromSome sn of
>                    Just p -> return $ f2 p
>                    _ -> error "Input if larger than 255"
> 

> f2 :: (c ~ (n <= 255)) => Proof n c -> ()
> f2 _ = ()
qnikst
code Haskell typefun
смотрите какая классная штуковина:

{-# LANGUAGE GADTs #-}
import Data.Dependent.Map as D
import Data.GADT.Compare

import GHC.Generics

data Hint a where
  HintPort   :: Hint Int
  HintHost   :: Hint String
  HintTeapot :: Hint Int

instance GEq Hint where
  HintPort `geq` HintPort = Just Refl
  HintHost `geq` HintHost = Just Refl
  HintTeapot `geq` HintTeapot = Just Refl
  _ `geq` _ = Nothing

instance GCompare Hint where
  HintPort `gcompare` HintPort = GEQ
  HintHost `gcompare` HintHost = GEQ
  HintTeapot `gcompare` HintTeapot = GEQ
  HintPort `gcompare` HintHost = GGT
  HintPort `gcompare` HintTeapot = GGT
  HintHost `gcompare` HintTeapot = GGT
  a `gcompare` b = case b `gcompare` a of
                     GEQ -> GEQ
		     GGT -> GLT
		     GLT -> GGT

fibs = 1:1:zipWith (+) fibs (tail fibs)

test :: DMap Hint
test = D.insert HintTeapot 7 $ D.insert HintPort 99 $ D.insert HintPort 7 D.empty

и потом:

*Main> test ! HintPort
99
*Main> test ! HintTeapot
7
*Main> test ! HintHost
"*** Exception: DMap.find: element not in the map
*Main> HintHost `D.lookup` test
Nothing


ещё бы инстансы автоматом генерить (хотя это наверняка в либе есть)
qnikst
? code Haskell typefun
Помогите пожалуйста понять принцип работы forall с type families.
Ниже минимальный пример неработающего кода, интересует метод foo.
Особенно интересует то, что обозначает явное задание сигнатуры для 
foob в методе foo, с одной стороны FooE неинъективно и соотв компилятор не может выбрать конкретное foob, с другой a и b внесены под forall что должно быть подсказкой копилятору.
Я так понимаю данное поведение зависит от следующего, FooE это функция из a b в элементы с kind *, соотвественно если на момент определения инстанса вместо FooE a b подставляется результат вычисления FooE a b, то получается то поведение, что мы видим (тип b финкирован результатом), а 'a' не определено.
Если же редуцирования (?) не происходит, то тогда инстанс должен быть выбран.
Соответсвенно вопросы:
1. правильны ли те предположения, что я написал выше
2. куда почитать, чтобы подтвердить их или опровергнуть
3. это баг или фича

--
да, я знаю, что с data families все будет работать.


{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}

class FooC a b where
  type FooE a b
  foob :: FooE a b -> b

foo :: forall a b . FooC a b => [FooE a b] -> b
foo = map (foob :: FooE a b -> b)

вывод:
3.hs:9:8:
    Could not deduce (FooE a0 b ~ FooE a b)
    from the context (FooC a b)
      bound by the type signature for foo :: FooC a b => [FooE a b] -> b
      at 3.hs:9:8-47
    NB: ‘FooE’ is a type function, and may not be injective
    The type variable ‘a0’ is ambiguous
    Expected type: [FooE a b] -> b
      Actual type: [FooE a0 b] -> b
qnikst
? Haskell typefun у меня проблема я хочу написать класс типов:

class CanInsert x y where
insert :: x -> y -> InsertResult x y

type family InsertResult x y :: *
type instance InsertResult x (CustomSetG '[]) = CustomSetG (x ': '[])
type instance InsertResult x (CustomSetG (y ': ys)) = If (x == y) (CustomSetG (x ': ys)) (CustomSetG (y ': InsertResult x ys))

тут проблема в ветке false т.к. InsertResult x ys :: * то оно не вставляется в ': и не promot-ится т.к. нет конструктора

если я уберу CustomSetG то вопрос, как вернуть результат с kind [*]:


type family InsertResult x y :: [*]
type instance InsertResult x (CustomSetG '[]) = (x ': '[])
type instance InsertResult x (CustomSetG (y ': ys)) = If (x == y) ( (x ': ys)) ((y ': InsertResult x ys))

?
qnikst
code Haskell хочется_странного typefun
есть

data HList :: [*] -> * where
  HNil :: HList '[]
  :>    :: t -> HList ts -> HList (t ': ts)

хочу написать тип:

data C t a b = forall s . <magic-here> => C !s (a -> s -> (b,s))

где <magic-here> должно обозначать следующее, каждый элемент в (HList s) должен быть элементом класса VectorSpace.

Напр запись <magic-here> VectorSpace t (HList s), будет говорить, что весь HList является VectorSpace, что в свою очередь будет обозначать что каждый элемент списка тоже VectorSpace..

В принципе есть хак, который мне не очень нравится, сделать

data HList :: * -> [*] -> * where
  HNil :: HList a '[]
  (:>) :: VectorSpace a t => t -> HList ts -> HList a (t':ts)

это классно сработает, но данное решение обозначает, что я не могу использовать HList из других либ и придётся таскать свой.
qnikst
Haskell typefun вот я недавно в игрушечном примере делал typelevel floating point через предел type level rational, которые представляются как два type level integer. в это время можно делать через a/2^e, где a и e этот Integer. вопрос когда какое представление удобнее?
qnikst
? Haskell typefun а чего у меня rewrite rule не заводятся?

newtype Tagged n s = Tagged n

sort2 :: Ord a => Tagged [a] s -> Tagged [a] Sorted
sort2 = Tagged . trace "sorting.." . List.sort . coerce
{-# NOINLINE[1] sort2 #-}

{-# RULES
"sort/Sorted" forall (x :: Tagged a Sorted). sort2 x = x
#-}

main = print $ sort2 . sort2 $ voidT [1..3]
qnikst
Haskell typefun {-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}

import Data.Proxy
import GHC.TypeLits

data S a = S a (S a)

data T n a = T a deriving (Show)

toProxy :: T n a -> Proxy n
toProxy _ = Proxy

mkT :: KnownNat n => proxy n -> a -> T n a
mkT _ a = T a

useT t@(T a) = fromIntegral (natVal (toProxy t)) + a

*Main> useT $ mkT (Proxy :: Proxy 4) 0.5
4.5

так, то! в то время как космические питоны бороздят просторы динамического варианта, мы храним значения в типах!
qnikst
Haskell typefun (интересно я уже всех тут достал) есть:

data M = A | B

getSingletons [''M]

data S :: (M -> *) where

есть Ptr (S a), могу ли я по Ptr (S a) выдернуть синглетон?


пока писал понял как сделать это с проксёй
qnikst
? code Haskell typefun
есть у меня метод:


hexp :: S s a -> H s a

но он не совсем верен, на самом деле он должен выглядеть как:

hexp :: S s a -> H s a -- для тех `a` которые не будут выведены в конретный тип по S s a
hexp :: S s a -> H s b -- во всех остальных случаях.

Реально ли?
qnikst
? code Haskell typefun
про категории и регионы, т.е. тот пост, что был днём ранее, в итоге у меня получилось следующее:

[там внизу вопрос ещё будет про type families и type classes, так что если интересно мне помочь, то всю эту писанину можно и пропустить]

A.hs:
{-# LANGUAGE UndecidableInstances #-}
-- Вариант для чистого преобразования
type CanReleasePure s g = CanRelease s g IO

-- Правило позволяющее определить свой порядок
type family IsAncestor a b (c :: * -> *) :: Bool

-- Правило описывающее поведения "начального" и "терминального" элементов
type family CanRelease s g (m :: * -> *) where
  CanRelease G x y = True
  CanRelease x V y = True
  CanRelease a b c  = IsAncestor a b c

B.hs: -- тут собственно вводится мой трансформер

-- Правило для спуска по монадному стеку и проверка
type family IsAncestor2 a (m :: * -> *) :: Bool where
   IsAncestor2 a IO = False
   IsAncestor2 a (R m s) = a == s || IsAncestor a m

-- Правило проверяющее, что можно будет кастовать только к
-- только внешнему типу (можно былоб убрать, если в type family 
-- в A.hs добавить Constraint
type instance IsAncestor s g (R m s') = (g == s') || IsAncestor2 s (R m s')
---------------------------------------------------------------------------

В общем-то то неплохо, хотя и замучено, пользователь библиотеки,
конечно весь этот ад не увидит, в его распоряжении будет только

CanReleasePure a b
ну и функции это использующие:

release :: CanReleasePure a b ~ True => S a c -> S b c
releaseM :: (MonadR m, CanRelease a (Region m) m ~ True) => S a c -> m (S (Region m) c
-----------------------------------------------------------------------------

Так вот, всю эту радость можно реализовать и с помощью тайп классов,
тогда констрейн будет выглядеть просто как CanRelease .. без ~ True,
вопрос, тогда стоит что выбирать?