typefunspecialolympicHaskell
А давайте спецолимпиадку по типам? Есть код codegists.com это Freer для стрелок, но с ним проблема, нужно квадратичное число инстансов, так надо определять Category (Freer Category eff), Category (Freer Arrow eff), несмотря на то, что Category => Arrow. Что очевидно очень печально, и хотелось бы это поправить.
Есть чуть более простые варианты но с тоже с квадратичным числом инстансов, хоть и более простых. Так же можно запилить вариант на TH который будет сразу генерить полный instance search, но это читерство.
Принимаются варианты и предложения по улучшению гиста.
typefundependent-typesCS
И в догонку, допустим у меня есть линейный вектор, и я его сортирую; достаточно ли привести доказательства, что результирующая линейный вектор имеет тот же размер и сортирован.
Т.Е. Можно ли фактом использования линейных структур заменить доказательство того что новый вектор это перестановка элементов исходного?
ghctypefun
1.hs:16:1: error:
• Invalid declaration for ‘FieldType’; you must explicitly
declare which variables are dependent on which others.
Inferred variable kinds:
p :: N
t :: Type
i :: Fin p
• In the type synonym declaration for ‘FieldType’
data NS (f :: k -> *) (xs :: [k]) where
Z :: f x -> NS f (x ': xs)
S :: NS f xs -> NS f (x ': xs)
им, с каким-нить дополнительным констрейнтом, ведь можно выразить type-level set?
Причем даже с не самым неадекватным паттерн матчингом и проверкой того, что все заматчено.
есть reify с помощью него я могу протаскивать словарики в инстансы, в которые через instance head их не протолкнуть. у меня есть например:
```
withAcquire
:: forall m r.
(MonadR m)
=> (forall s. Reifies s (AcquireIO (Region m)) => Proxy s -> m r)
-> m r
withAcquire f = reify (AcquireIO (unsafeToIO . macquire)) f
where
macquire :: SEXP V a -> m (SEXP (Region m) a)
macquire = acquire
```
я хочу теперь тоже самое но работающее в чистом коде (для чистовекторов)
вот каким чудом это сделать непонятно:
```
withGlobalAcquire :: (forall s t . Reifies s (AcquireIO t) => Proxy s -> ST t r) -> r
withGlobalAcquire f = ST.runST $ reify (AcquireIO acquireIO) f
where
acquireIO :: SEXP V ty -> IO (SEXP t ty)
acquireIO x = do
R.preserveObject x
return $ R.unsafeRelease x
```
это работает, но есть проблема, что тип вектора определяется как ElemRep s v ty, т.к. у нас тут тип t из forall, то в итоге этот констрейнт нифига не добавить и что делать неясно
typefun?Haskell
Вот я хочу какую-то структуру, работающую как:
(Key -> Value Key) причем соотвествие Value Key задается в рантайме, т.е. у меня есть Free монатка, в которой написано, что-то вроде
intKey <- define "Key" read show (42::Int)
stringKey <- define "Key2" id id ("42"::String)
action $ do { x <- readValue intKey :: MyMonad Int ; y <- readValue stringKey :: MyMonad String ; ...
}
далее, внутри интерпретатора фримондки по декларациям должна создаться структура где будут положены значения по умолчанию (последний параметр define) и ещё в рантайме ему могут скидываться ("key","value") пары, соотв readValue должны считывать обновленные.
Вопрос, как это все сложить? У меня пока только идея сделать Data.Map String Any и немного unsafeCoerce (ну или +Typeable и coerce), что выглядит как-то печальненько.
typefunHaskell
В haskell чятике совершенно неожиданно выяснилось, что zipper-ы это производная от алгебраического представления типа, это ж круто! Так их понимать и писать на порядок удобнее.
СпецолимпиадаtypefunHaskell
Кто-нить хочет простенькую спецолимпиадку, задача написать функцию с двумя ветками, одна ветка с эффектами (IO), а другая чистая.
type family SortI a b where
SortI '[] b = b
SortI (a:?n ': as) '[] = SortI as '[ a :? n]
SortI (a:?n ': as) bs = SortI as (Insert (a:?n) bs)
type family Insert a b where
Insert (a :? n) '[] = '[ a :? n ]
Insert (a :? n) ( b :? m ': bs) = UnOrdering (CmpSymbol n m)
((a :? n) ': (b :? m) ': bs)
((a :? n) ': (b :? m) ': bs)
((b :? m) ': Insert (a :? n) bs)
type family UnOrdering x a b c where
UnOrdering LT a b c = a
UnOrdering EQ a b c = b
UnOrdering GT a b c = c
typefun:(?Haskell
а что две переменные, которые forall нельзя сравнить, т.е.
если есть forall s1 s2 . IORT s1 (IORT s2 IO), то написать s1 == s2 нельзя?
typefunненужный_постHaskell
не выводятся результаты семейства классов? вылезают бесконечные типы? а ничего развернем стек в typelevel список стеков, и будем бегать по нему, не углубляясь в сравнение типа и тем самым не создавая бесконечные типы и вместо этого проходясь по списку. (type mastery + 2 пикаолега)