← All posts tagged typefun

А давайте спецолимпиадку по типам? Есть код codegists.com это Freer для стрелок, но с ним проблема, нужно квадратичное число инстансов, так надо определять Category (Freer Category eff), Category (Freer Arrow eff), несмотря на то, что Category => Arrow. Что очевидно очень печально, и хотелось бы это поправить.

У меня получилось такое:

gist.github.com

Есть чуть более простые варианты но с тоже с квадратичным числом инстансов, хоть и более простых. Так же можно запилить вариант на TH который будет сразу генерить полный instance search, но это читерство.

Принимаются варианты и предложения по улучшению гиста.

И в догонку, допустим у меня есть линейный вектор, и я его сортирую; достаточно ли привести доказательства, что результирующая линейный вектор имеет тот же размер и сортирован.
Т.Е. Можно ли фактом использования линейных структур заменить доказательство того что новый вектор это перестановка элементов исходного?

чего-то я совсем тупой стал.. есть:

data F = A | B | C

есть

data M (a::F) = M (Ptr (M a))

есть

data SM = forall a . M a

есть (по смыслу)

typeOf :: SM -> F

какой магией тепеь сделать case split по SM так чтобы было что-то вроде:

case typeOf sm of
A -> тут бы выводилось, что у нас M a

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’


А вот как это явно указать?

вот я смотрю на n-ary choice:

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, то в итоге этот констрейнт нифига не добавить и что делать неясно

Вот я хочу какую-то структуру, работающую как:
(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), что выглядит как-то печальненько.

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

и немного кметтизма:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

data A = A
data B = B

data X a b where
X :: a -> X a B
Y :: a -> X a A

newtype Foo a = Foo (forall c. X a c -> c)

go :: forall a c . X a c -> c — интересно тут
go (X x) = concrete1 x
go (Y y) = concrete2 y

concrete1 :: a -> B
concrete1 _ = B
concrete2 :: a -> A
concrete2 _ = A

В продолжение #2792430

*Record> mkGA2 (Proxy :: Proxy "B") 4 (Proxy :: Proxy "A") 'c'
{A: 'c', B: 4, }

и даже так:

foo :: (Sort '[ Int :? na, Char :? "C"] ~ z, KnownNat (FieldIndex na z), KnownNat (FieldIndex "C" z)) => Proxy na -> ARec z
foo p = mkGA2 p (4::Int) (Proxy :: Proxy "C") 'c'

*Record> foo (Proxy :: Proxy "A")
{A: 4, C: 'c' }
*Record> foo (Proxy :: Proxy "D")
{C: 'c', D: 4}

Теперь бы сделать вариативную строгость с инфой в типах, а потом выкинуть все нафиг и использовать fixed-vector-hetero

```
*Record> :kind! Sort '[Int :? "foo", String :? "bar"]
Sort '[Int :? "foo", String :? "bar"] :: [*]
= '[[Char] :? "bar", Int :? "foo"]
```

как можно это проще сделать?

type Sort a = SortI a '[]

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

не выводятся результаты семейства классов? вылезают бесконечные типы? а ничего развернем стек в typelevel список стеков, и будем бегать по нему, не углубляясь в сравнение типа и тем самым не создавая бесконечные типы и вместо этого проходясь по списку. (type mastery + 2 пикаолега)