MarcelineVQ

lookup: (m: List (k, v)) -> (key: k) -> Dec (val: v ** Elem (key, val) m)
lookup [] key = No ?foo
lookup (x :: xs) key = ?lookup_rhs_2

MarcelineVQ

package-indices:
- name: Tsinghua
  download-prefix: http://mirrors.tuna.tsinghua.edu.cn/hackage/
  http: http://mirrors.tuna.tsinghua.edu.cn/hackage/00-index.tar.gz
  hackage-security:
    keyids: []
    key-threshold: 0

MarcelineVQ

λ :t toListOf (types @(Name SrcSpanInfo)) g

<interactive>:1:11: error:
    • No instance for (Data.Generics.Product.Types.HasTypes'
                         (Data.Generics.Product.Types.Snd
                            (Data.Generics.Product.Types.InterestingOr
                               (Data.Generics.Product.Types.InterestingOr
                                  (Data.Generics.Product.Types.InterestingOr
                                     (Data.Generics.Product.Types.Interesting'
                                        (GHC.Generics.Rep (GHC.Real.Ratio Integer))

MarcelineVQ

<zeta_0> hello guys, i am currently learning category theory, i cannot find a good definition on what `covariant` and `contravariant` mean in terms of `category theory`, could you guys give my literal translations for `co`, `contra`, and `variant` and how they are used in category theory?
* heatsink_ ([email protected]) has joined
<pyan> zeta_0: “covariant” means “preserves the direction of the arrows”, and “contravariant” means “reverses the direction of the arrows”
* Saukk has quit (Remote host closed the connection)
<ski> "covariant" here means "varies in the same direction", while "contravariant" means "varies in the opposite direction"
* p0lyph3m has quit (Ping timeout: 250 seconds)
<ski> say `C',`D' are categories, `A',`B' are objects of `C', and `f : A >---> B' is a morphism of `C'
* heatsink has quit (Ping timeout: 264 seconds)
<ski> if `F' is a (covariant) functor from `C' to `D', then `F f : F A >---> F B'
* Jeanne-Kamikaze ([email protected]) has joined

MarcelineVQ

adjacent: (x, y : BitVector n) -> Dec (hammingDistance x y = 1)
adjacent x y with (hammingDistance x y)
  adjacent x y | Z = No (\Refl impossible)
  adjacent x y | (S Z) = Yes Refl
  adjacent x y | (S (S k)) = No (\Refl impossible)

MarcelineVQ

module Main where

{-# NOINLINE foo #-}
foo :: String
foo = "hello"

foo2 :: String
foo2 = "goodbye"

main :: IO ()

MarcelineVQ

<Ferdirand> i'm trying to define a type for lists of two alternating types
<Ferdirand> data Chain a b l where
<Ferdirand>     Nil  :: Chain a b b
<Ferdirand>     (:@) :: a -> Chain b a l -> Chain a b l
<Ferdirand> l represents the statically-known type of the last element
<Ferdirand> now, for the type Chain (a b a), which has the same type for the first and last element, i know that if a and b are different types, then the list cannot be empty
<Ferdirand> and i'd like to write a type-safe `last` function that reflects that

<Ferdirand> data Chain a b l where
<Ferdirand>     Nil  :: Chain a b b

MarcelineVQ

extra-deps:
- git: https://github.com/haskell/containers
  commit: 403cf3cb7ef365961269cebe9d4eeb7221edd927
  subdirs:
    - containers
    - containers-tests

MarcelineVQ

  ___
___ ___

MarcelineVQ

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Lib where

import Data.Char