Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Icelandjack / Braindump.hs
Last active Oct 15, 2018
For Chris Allen, braindump
View Braindump.hs
-- 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
View SystemF.hs
-- 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
Icelandjack / 14823.md
Last active Apr 5, 2018
#14832: QuantifiedConstraints: Adding to the context causes failure
View 14823.md

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
Icelandjack / TF_QC.md
Last active Sep 5, 2018
(#14860) QuantifiedConstraints: Can't quantify constraint involving type family
View TF_QC.md

For the Trac ticket #14860.

All these types are valid for h, but its principal type involves -XQuantifiedConstraints

{-# Language FlexibleInstances, MultiParamTypeClasses, GADTs, QuantifiedConstraints #-}

import Data.Kind

type family FB (a::Type) (b::Type) :: Type where
View gist:3a98d3979879fd9415bbde3761c51760
-- Response to
-- https://gist.github.com/sjoerdvisscher/e8ed8ca8f3b6420b4aebe020b9e8e235
-- https://twitter.com/sjoerd_visscher/status/975375241932427265
{-# Language QuantifiedConstraints, TypeOperators, RankNTypes, GADTs, ConstraintKinds, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, InstanceSigs #-}
import Data.Coerce
type f ~> g = forall x. f x -> g x
View 14733.hs
{-# Language QuantifiedConstraints #-}
{-# Language GADTs #-}
{-# Language ConstraintKinds #-}
{-# Language MultiParamTypeClasses #-}
{-# Language UndecidableSuperClasses #-}
{-# Language FlexibleInstances #-}
{-# Language UndecidableInstances #-}
{-# Language AllowAmbiguousTypes #-}
data D c where
@Icelandjack
Icelandjack / Twitter_Oleg.md
Last active Jan 30, 2018
Response to Oleg Grenrus
View Twitter_Oleg.md
View 14661.md
class ListLike f where
  nil  :: f a
  cons :: a -> f a -> f a
  (·)  :: f a -> f a -> f a

newtype LL a = LL (forall ff. ListLike ff => ff a)

instance ListLike LL where
  nil :: LL a
@Icelandjack
Icelandjack / OpenKinds.markdown
Last active Jan 26, 2020
Rethinking Tricky Classes: Explicit Witnesses of Monoid Actions, Semigroup / Monoid / Applicative homomorphisms
View OpenKinds.markdown