Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    klapaucius
    @klapaucius
    Пока что тут будет мой фп-микробложек
    Оказывается, в синонимах паттернов для рекордов нельзя инфиксные поля декларировать
    Узнал я об этом, обнаружив работы над тем, чтоб так делать было можно https://phabricator.haskell.org/D3379
    правда в этих паттернах синонимах для рекордов полно всего неработающего. Они в ghci 8.0 вообще не юзабельные
    но там и в 8.2 не все хорошо
    klapaucius
    @klapaucius
    Prelude> :set -XPatternSynonyms
    Prelude> pattern List { hd, tl } = hd:tl
    Prelude> :i hd
    hd :: [a] -> a  -- Defined at <interactive>:2:16
    Prelude> :set -XRecordWildCards
    Prelude> List {..} = [1..5]
    
    <interactive>:7:1: error:
        Illegal `..' notation for constructor ‘ListThe constructor has no labelled fields
    рекорд вайлдкардс не работают
    klapaucius
    @klapaucius
    Несдержался и написал ответ в достаточно тухлый уже спор на рсдн с имитацией идрисного кода на хаскеле:
    {-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, GADTs #-}
    {-# LANGUAGE TypeOperators, NPlusKPatterns #-}
    {-# LANGUAGE DeriveFoldable, StandaloneDeriving, TypeApplications #-}
    {-# LANGUAGE TemplateHaskell #-} 
    
    import Data.Singletons
    import Data.Singletons.TH
    
    import Text.Read (readMaybe)
    import Data.Kind (Type)
    import qualified Data.Foldable as F
    
    data Nat = Z | S Nat deriving Show
    
    intToNat 0 = Z
    intToNat (n + 1) = S (intToNat n)
    
    genSingletons [''Nat]
    
    -- генерирует синглетоны для Nat:
    
    -- data instance Sing (n :: Nat) where
    --     SZ :: Sing Z
    --     SS :: Sing n -> Sing (S n)
    
    -- instance SingKind Nat where
    --     type DemoteRep Nat = Nat
    
    --     fromSing SZ = Z
    --     fromSing (SS b) = S (fromSing b)
    
    --     toSing Z = SomeSing SZ
    --     toSing (S b) = case toSing b :: SomeSing Nat of
    --           SomeSing c -> SomeSing (SS c)
    
    data Vect :: Nat -> Type -> Type where
       V0 :: Vect Z x
       (:>) :: x -> Vect n x -> Vect (S n) x
    
    deriving instance Foldable (Vect n) 
    
    infixr 5 :>
    
    getInt :: IO Int
    getInt = do
      resp <- getLine
      case readMaybe @Int resp of
         Just value -> pure value
         Nothing -> do
           putStrLn "error"
           getInt
    
    makeVect :: Sing (size :: Nat) -> a -> Vect size a
    makeVect SZ _ = V0
    makeVect (SS x) v = v :> makeVect x v
    
    zipVect :: Vect size a -> Vect size b -> Vect size (a, b)
    zipVect V0 V0 = V0
    zipVect (x1 :> v1) (x2 :> v2) = (x1, x2) :> zipVect v1 v2
    
    main :: IO ()
    main = do
      putStrLn "Hello world"
      size <- getInt
      -- нету "голых" экзистенциальных типов, 
      -- работать с синглетоном числа придется только в континьюэйшене
      withSomeSing (intToNat size) $ \ssize -> do
        let vect1 = makeVect ssize size
        let vect2 = makeVect ssize "^_^"
        -- let vect2 = makeVect (SS ssize) "^_^" -- вызовет ошибку
        print . F.toList $ vect1
        print . F.toList $ vect2
        print . F.toList $ zipVect vect1 vect2
    klapaucius
    @klapaucius
    Диссер Марка Джонса (вроде бы про баундед полиморфизм, тайпклассы, расширяемые рекорды, сабтайпинг, вот это вот все , пока не читал ) https://www.cs.ox.ac.uk/files/3432/PRG106.pdf
    klapaucius
    @klapaucius
    Лещинский считает синонимы паттернов ошибкой, а Марлоу считает ошибкой вью паттерны
    klapaucius
    @klapaucius
    ghc/ghc@26c95f4
    klapaucius
    @klapaucius
    ghc/ghc@bf5e0ea
    klapaucius
    @klapaucius
    в этот раз буду разговаривать с банано-линзо-телевизором в персональном гиттер-чатике специально для таких излияний
    klapaucius
    @klapaucius
    "полноценность", думаю, все равно останется дискуссионной
    сейчас-то надо вообще фактически три раза писать - для значений, типов и синглетонов.

    основная разница все же не в тайп ин тайп а в

    Separation between terms and coercions.
    Because the term language may not terminate, DC coercions
    come from a separate, consistent language for reasoning about equality in DC. Propositional equalities
    are witnessed by coercions instead of computational proofs. This distinction means that coercions are
    not relevant at runtime and may be erased. Furthermore, DC’s form of propositional equality has a avor
    of extensional type theory (Martin-Löf 1984)—equality proofs, even assumed ones, can be used without
    an elimination form

    тайп-ин-тайп и в агде вроде включается
    так, перерыв
    klapaucius
    @klapaucius
    для этого и завтипы не обязательны
    ну так gadt это и есть такая "дорожка наверх"
    почему для простейших-то?
    klapaucius
    @klapaucius
    это хуже нормальных завтипов тем что 1 ) писать код три раза см.выше 2) "доказательства" обязательно выполнять
    klapaucius
    @klapaucius
    c Вадлером в одной конторе работает теперь
    klapaucius
    @klapaucius
    Хаскель индустриальный с тех пор, когда появились люди, которые вынуждены писать на нем а не на том, на чем они хотели бы. Года 4 назад видел такого страдальца из селектела или как там его в окамлоджаббере
    klapaucius
    @klapaucius
    число людей, написавших половину гхц известно - ноль.
    не слышал хаскелькаст, но читал часть (полностью - это нереально, конечно) ковровой бомбардировки Остина на реддите по мотивам
    klapaucius
    @klapaucius
    уже на 8.2 портировать пора
    klapaucius
    @klapaucius
    Я так понимаю, что 8.0.2 обратно несовместим с 8.0.1
    Было у нас, к примеру FooBarClass a => a -> a потом как-то все это рефакторилось и осталось что-то вроде FooBarClass a => FooBar -> FooBar понятно, что контекст больше не нужен, но про него забыли
    8.0.1 компилирует без вопросов, а 8.0.2 не хочет, типы, говорит, противоречиво-неопределенные.
    Я все понимаю, хаскель - но для минорной версии это перебор уже
    klapaucius
    @klapaucius

    сквозь мрачные затворы глас доходит не только в каторжные норы, но и из каторжных нор:

    https://youtu.be/9SOFqWYpf9Y?t=70

    klapaucius
    @klapaucius
    Last year, the GHC developers announced that GHC 8.2 would primarily be a "consolidation release", with a focus on bugfixing and performance improvements. Did this ambition actually pan out?
    хахахахаха нет
    Leonid Onokhov
    @sopvop
    вот да
    Alexander Vershilov
    @qnikst
    как будто кто-то ожидал другого?
    klapaucius
    @klapaucius
    уверен, что много кто ожидал. Как же так вышло, что ожидал - другой вопрос
    но я уже привык к тому, что много странных вещей люди ожидают
    klapaucius
    @klapaucius
    {-# RULES
    "plusCommutative" forall m n. plusCommutative m n = unsafeCoerce (Refl :: 'Z :~: 'Z)
    "plusZero" forall m . plusZero m = unsafeCoerce (Refl :: 'Z :~: 'Z)
    "plusSucc" forall m n. plusSucc m n = unsafeCoerce (Refl :: 'Z :~: 'Z)
    "plusAssoc" forall m p1 p2. plusAssoc m p1 p2 = unsafeCoerce (Refl :: 'Z :~: 'Z)
     #-}
    klapaucius
    @klapaucius
    половина из всего занимаемого установленными планинами для vs code места - гифы с демонстрациями возможностей идрисного плагина
    klapaucius
    @klapaucius

    Отзыв о клине от одного из двух известных мне программистов (хеллоуворлдов, но там другого и не написать) на нем - Попова.

    Clean's unique types are often extremely awkward to use, for example when you need to mutate some unique values in an array, so "industrial utility and value" for Clean is probably not that big. Last time I checked Clean's GC was extremely simple and stupid (two-space Cheney dividing heap in halves and copying all the live data back and forward, if there is some free space, and if free memory is scarce, switch to another GC that moves data inside one space), no use of uniqueness in GC. Even worse, uniqueness allowed to mutate records in place without having to copy them, but for some reason Clean missed this optimization and blindly copied the whole record when you change one field in it, leaving the old value as garbage. Only arrays were mutated in-place.

    второй - Балин, если кому-то вдруг не все равно