Icelandjack

Solving Trac ticket #14832:

{-# Language QuantifiedConstraints, ScopedTypeVariables, TypeOperators, GADTs, FlexibleInstances, UndecidableInstances, ConstraintKinds, MultiParamTypeClasses, InstanceSigs, TypeApplications #-}

import Prelude hiding (id, (.))
import Control.Category
import Data.Coerce

data Dict c where

Icelandjack

Nested

Showing where types change:

infixr 5 :::
data Nest a = N | a ::: Nest (a, a)

In

Icelandjack

-- type Sig k = [k] -> Type
-- 
-- data AST :: Sig k -> Sig k where
--   Sym  :: dom a -> AST dom a
--   (:$) :: AST dom (a:as) -> AST dom '[a] -> AST dom as

singletons [d| data N = O | S N |]

infixr 5 :·
data Vec :: N -> Type -> Type where

Icelandjack

data Kl_kind :: (Type -> Type) -> Type where
  Kl :: Type -> Kl_kind(m)
  
type family
  UnKl (kl :: Kl_kind m) = (res :: Type) | res m -> kl where
  UnKl (Kl a) = a

Icelandjack

{-# Language RankNTypes              #-}
{-# Language LambdaCase              #-}
{-# Language TypeOperators           #-}
{-# Language TypeApplications        #-}
{-# Language PolyKinds               #-}
{-# Language TypeFamilies            #-}
{-# Language FlexibleInstances       #-}
{-# Language GADTs                   #-}
{-# Language ConstraintKinds         #-}
{-# Language MultiParamTypeClasses   #-}

Icelandjack

Interesting https://www.reddit.com/r/haskell/comments/1u8rp1/with_two_different_functors/

Description of monoidal natural transformations https://gist.github.com/Icelandjack/9e6902690a244286843164e554a8c3db

Icelandjack

https://mail.haskell.org/pipermail/haskell-cafe/2010-November/086055.html

http://conal.net/blog/posts/simplifying-semantics-with-type-class-morphisms

http://conal.net/blog/posts/another-lovely-example-of-type-class-morphisms

https://arxiv.org/pdf/1202.2919.pdf

eta (pure c) = pure c

Icelandjack

-- SYSTEM F
--   http://homepages.inf.ed.ac.uk/slindley/papers/embedding-f.pdf
-- 
-- Type-level lambdas
--   https://gist.github.com/AndrasKovacs/ac71371d0ca6e0995541e42cd3a3b0cf


{-# language TemplateHaskell, ScopedTypeVariables, RankNTypes,
             TypeFamilies, UndecidableInstances, DeriveFunctor, GADTs,
             TypeOperators, TypeApplications, AllowAmbiguousTypes,

Icelandjack

I was implementing "variable-arity zipWith" from Richard Eisenberg's thesis (recommended) when I noticed it used

apply :: [a -> b] -> [a] -> [b]
apply (f:fs) (a:as) = f a : apply fs as
apply _      _      = []

and

repeat :: a -> [a]

Icelandjack

-- https://www.reddit.com/r/haskell/comments/abxem5/experimenting_with_kleisli_instance_of/

{-# Language TypeApplications     #-}
{-# Language RankNTypes           #-}
{-# Language DataKinds            #-}
{-# Language KindSignatures       #-}
{-# Language PolyKinds            #-}
{-# Language TypeOperators        #-}
{-# Language GADTs                #-}
{-# Language TypeFamilies         #-}