Icelandjack

https://github.com/phadej/metametapost/tree/34eb0d757655d15317d58f549e9cf4c794cff79e/src/MetaMetaPost

• https://github.com/phadej/metametapost/blob/34eb0d757655d15317d58f549e9cf4c794cff79e/src/MetaMetaPost/Simplifier.hs

simplify :: Expr SomePrim (Type s) a -> Either String (MP s a)
simplify (Var a)                = pure (MPApp (MPVar a))
simplify (Prim (SomePrim p))    = simplifyPrim0 p
simplify (Lam _ _)              = throwError "Non-applied lambda abstraction"

Icelandjack

Motivating examples for https://ghc.haskell.org/trac/ghc/ticket/10843, https://ghc.haskell.org/trac/ghc/wiki/ArgumentDo

This should allow

curry $ \case

without the dollar giving us weird code

Icelandjack

To allow hask

type Cat k = k -> k -> Type

type Fun i j = i -> j

data Nat :: Cat i -> Cat j -> Cat (Fun i j) where
  Nat :: (FunctorOf cat cat' f, FunctorOf cat cat' f') => (forall a. Ob cat a => cat' (f a) (f' a)) -> Cat cat cat' f f'

Icelandjack

https://www.reddit.com/r/haskell/comments/6i7nil/kinderfunctor_using_typeintype_with_a_polykinded/

Icelandjack

Principle of identity expansion

Whenever some construction has a certain relationship to all constructions of the same kind within a category, it must, in particular, have this relationship to itself. Socrates’ dictum to “know thyself” is as important in category theory as it is in life. So whenever we encounter a universal construction we will see what we can learn about it by “probing it with itself”. In the case of a terminal object, this means choosing X ≔ T in the definition.

Lemma 3.1.1.2 (identity expansion for terminals) If T is a terminal object then !(T) = id(T).

Lemma 3.1.4.2 (identity expansion for initials) If S is an initial object then ¡(S) = id(S).

Icelandjack

{-# Language InstanceSigs, ViewPatterns, TupleSections, GeneralizedNewtypeDeriving, TemplateHaskell, LambdaCase #-}

module D where

import Language.Haskell.TH
import Data.Coerce

deriveVia :: Name -> Name -> Name -> Q [Dec]
deriveVia className ty viaNewTy = do
  a <- reify className

Icelandjack

Compare https://twitter.com/mrkgnaow/status/876007524968800256 to Haskell, should probably stress this before each talk

This is a list of different ways of thinking about or conceiving of the derivative, rather than a list of different logical definitions. Unless great efforts are made to maintain the tone and flavor of the original human insight, the differences start to evaporate as soon as the mental concepts are translated into precise, formal and explicit definitions.

I can remember absorbing each of those concepts as something new and interesting, and spending a good deal of mental time and effort digesting and practicing with each, reconciling it with the others. I also remember coming back to revisit these different concepts later with added meaning and understanding.

Icelandjack

type Cat k = k -> k -> Type

data T = D | I

type family
  Interp (a :: T) :: Type where
  Interp I = Int
  Interp D = Double

data Fn :: (T, T) -> Type where

Icelandjack

http://www.eduhk.hk/cte2017/doc/CTE2017%20Proceedings.pdf#page=138

Computational thinking has attracted a lot of attention worldwide in recent years since the publication of Jeannette M. Wing’s (2006) highly influential paper in the Communications of the ACM, in which she argues that the way computer scientists think about the world is useful in other contexts. Wing writes:

Computational thinking involves solving problems, designing systems, and understanding human behavior, by drawing on the concepts fundamental to computer science. Computational thinking includes a range of

Icelandjack

Ticket #12001.

Data.List.NonEmpty

pattern Singleton :: a -> NonEmpty a
pattern Singleton a <- (uncons -> (a, Nothing))
  where Singleton a = a N.:| []

infixr 5 :|