Instantly share code, notes, and snippets.

View coerceDict.hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
View gvalidate.hs
{-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeApplications, MultiParamTypeClasses, GADTs #-}
import Generics.OneLiner.Binary
import Data.Functor.Identity
class IsMaybe s s' where isMaybe :: s -> Maybe s'
instance (s ~ Maybe s') => IsMaybe s s' where isMaybe = id
validate
:: (ADT (f Maybe) (f Identity), Constraints (f Maybe) (f Identity) IsMaybe)
View laws.hs
{-# LANGUAGE
TypeFamilies
, KindSignatures
, ScopedTypeVariables
, ConstraintKinds
, FlexibleInstances
, FlexibleContexts
, DeriveGeneric
, DeriveAnyClass
, TypeApplications
View hfree example.hs
{-# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts, RankNTypes, GADTs, TypeOperators, UndecidableInstances, ConstraintKinds, DataKinds , ScopedTypeVariables #-}
import Data.Constraint
import Data.Constraint.Class1
import Data.Functor.HFree
class BaseSem sem where
val :: a -> sem a
add :: sem Int -> sem Int -> sem Int
View basesem2.hs
{-# LANGUAGE TypeFamilies, FlexibleInstances, RankNTypes, GADTs #-}
class BaseSem sem where
val :: a -> sem a
add :: sem Int -> sem Int -> sem Int
iff :: sem Bool -> sem a -> sem a -> sem a
gte :: sem Int -> sem Int -> sem Bool
expr :: BaseSem sem => sem Int
expr = iff (gte (val 10) (val 20)) (val 100) (val 200)
View basesem.hs
{-# LANGUAGE TypeFamilies, FlexibleInstances, RankNTypes, GADTs #-}
import Data.Functor.HFree
class BaseSem sem where
val :: a -> sem a
add :: sem Int -> sem Int -> sem Int
iff :: sem Bool -> sem a -> sem a -> sem a
gte :: sem Int -> sem Int -> sem Bool
View zeros.hs
{-# LANGUAGE DeriveAnyClass, DerivingStrategies, DefaultSignatures, TypeApplications, FlexibleContexts, DeriveGeneric #-}
import GHC.Generics
import Generics.OneLiner (nullaryOp, ADTRecord, Constraints)
class Zeros z where
zero :: z
default zero :: (ADTRecord z, Constraints z Zeros) => z
zero = nullaryOp @Zeros zero
{-# INLINE zero #-}
View sem.hs
{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances #-}
{-# LANGUAGE LambdaCase, FlexibleContexts, UndecidableInstances, TypeOperators, DataKinds, MultiParamTypeClasses #-}
module Sem where
import Data.Algebra
import Data.Constraint
import Data.Constraint.Class1
import Data.Functor.Free
class BaseSem a where
View leftadj-rep-iso.hs
rep2left :: Adjunction f u => Rep u -> f ()
rep2left = index (unit ())
left2rep :: Adjunction f u => f () -> Rep u
left2rep = rightAdjunct (const askRep)
iso :: Adjunction f u => Iso' (Rep u) (f ())
iso = dimap rep2left (fmap left2rep)
View geoalg.hs
{-# LANGUAGE
GADTs
, DataKinds
, InstanceSigs
, ViewPatterns
, TypeFamilies
, TypeOperators
, TypeApplications
, FlexibleInstances
, StandaloneDeriving