Lysxia

fmap :: ... => (a -> b) -> (f a -> f b)
(.) :: (y -> z) -> (x -> y) -> (x -> z)

fmap :: (f2 a -> f2 b) -> (f1 (f2 a) -> f1 (f2 b))
fmap ::                                                 (a -> b) -> (f2 a -> f2 b)
(.) :: (y              -> z                       ) -> (x        -> y             ) -> (x        -> z                       )
(.) :: ((f2 a -> f2 b) -> (f1 (f2 a) -> f1 (f2 b))) -> ((a -> b) -> (f2 a -> f2 b)) -> ((a -> b) -> (f1 (f2 a) -> f1 (f2 a)))
(.)    fmap                                            fmap ::                          (a -> b) -> (f1 (f2 a) -> f1 (f2 b))
^--- (.) fmap fmap = fmap . fmap

Lysxia

{-# LANGUAGE
    RankNTypes,
    ScopedTypeVariables,
    KindSignatures,
    GADTs
  #-}

import Data.Foldable (for_)
import System.IO (hFlush, stdout)

Lysxia

{-# LANGUAGE
    DeriveGeneric,
    FlexibleContexts,
    FlexibleInstances,
    ScopedTypeVariables,
    TypeFamilies,
    TypeOperators
    #-}

import GHC.Generics

Lysxia

Fixpoint map_intersperse_2
         (A B : Type) (f : A -> B) (c : A) (l : list A) {struct l} :
  map f (intersperse _ c l) = intersperse _ (f c) (map f l)  :=
  match l with
  | [] => eq_refl
  | h :: t =>
    let foo := map_intersperse_2 _ _ f c t in
    match t as t0
          return

Lysxia

Checking A (/home/sam/random/A.agda).
 Checking Data.Product (/usr/share/agda/lib/stdlib/Data/Product.agda).
  Checking Function (/usr/share/agda/lib/stdlib/Function.agda).
   Checking Level (/usr/share/agda/lib/stdlib/Level.agda).
Failed to write interface /usr/share/agda/lib/stdlib/Level.agdai.
/usr/share/agda/lib/stdlib/Function.agda:9,13-18
/usr/share/agda/lib/stdlib/Level.agdai: removeLink: permission
denied (Permission denied)

Lysxia

---
title: Naming abstraction
description: Abstract naming
keywords: Haskell, names, quiz
---

\begin{code}
{-# LANGUAGE GADTs, NoImplicitPrelude #-}
module Naming.Abstraction where
\end{code}

Lysxia

{-# LANGUAGE FlexibleInstances #-}

instance {-# OVERLAPPING #-} Show String where
  show = id

test :: Show a => [a] -> String
test = show

Lysxia

Inductive unitS : unit -> Type := ttS : unitS tt.
Definition ttS_unique : forall x, x = ttS :=
  fun x =>
    match x in unitS uu
            return match uu return unitS uu -> _ with
                   | tt => fun x => x = ttS
                   end x
    with
    | ttS => eq_refl
    end.

Lysxia

data Status = Expired | Valid
data SStatus (_ :: Status) where
  SExpired :: SStatus 'Expired
  SValid :: SStatus 'Valid
  
data Node (s :: Status) =
  { ...
  , anStatus :: SStatus s
    ...
  }

Lysxia

{-# LANGUAGE
    DataKinds,
    FlexibleInstances,
    FlexibleContexts,
    PolyKinds,
    ScopedTypeVariables,
    TypeApplications,
    TypeFamilies,
    TypeInType,
    TypeOperators #-}