Last active
April 10, 2019 04:58
-
-
Save greatBigDot/5a882e6361eb235ca6e085c625e659f2 to your computer and use it in GitHub Desktop.
A failed attempt to represent implicit proof terms in quasi-dependent Haskell.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE LambdaCase, EmptyCase | |
, EmptyDataDecls, TypeOperators, LiberalTypeSynonyms, | |
ExistentialQuantification, GADTSyntax, GADTs | |
, StandaloneDeriving | |
, InstanceSigs, FlexibleContexts, MultiParamTypeClasses, | |
FlexibleInstances , TypeSynonymInstances , FunctionalDependencies | |
, TypeFamilies, TypeFamilyDependencies, DataKinds, PolyKinds, | |
NoStarIsType , ConstraintKinds, QuantifiedConstraints , RankNTypes | |
, ExplicitForAll, KindSignatures, ScopedTypeVariables, | |
TypeApplications, ImplicitParams #-} | |
{-# LANGUAGE TemplateHaskell #-} | |
-- {-# LANGUAGE AllowAmbiguousTypes #-} | |
-- {-# LANGUAGE UndecidableInstances #-} | |
module Implicit () where | |
import Data.Kind | |
import Data.Singletons.TH | |
import Data.Constraint | |
-- | Define the natural numbers recursively and do all the singletons/promotion | |
-- stuff to it: | |
$(singletons [d| | |
data Nat :: Type where | |
Z :: Nat | |
S :: Nat -> Nat | |
|]) | |
-- | The family of the types of finite sets. | |
data Fin :: Nat -> Type where | |
FZ :: Fin (S n) | |
FS :: Fin n -> Fin (S n) | |
-- For whatever reason, `singletons` can't singletonize GADTs like `Fin`; in | |
-- case it's useful, see the bottom of this file for explicit implementations of | |
-- it. | |
data family (x :: a) !< (y :: a) :: Type | |
data instance (m :: Nat) !< (n :: Nat) where | |
LTZ :: Z !< S n | |
LTS :: m !< n -> S m !< S n | |
class (x :: a) &< (y :: a) where | |
lt_proof :: x !< y | |
instance Z &< S n where | |
lt_proof = LTZ | |
instance m &< n => S m &< S n where | |
lt_proof = LTS lt_proof | |
-- Doesn't work: | |
inj :: ∀ (m :: Nat) (n :: Nat). (m &< n) => SNat m -> SNat n -> Fin n | |
inj SZ (SS _) = FZ -- Fine; the `Z &< S n` instance gets the job done | |
inj (SS n') (SS m') = FS (inj n' m') -- Everything breaks; the proof is uninferrable | |
-- We get: | |
{- | |
• Could not deduce (n1 &< n2) arising from a use of ‘inj’ | |
from the context: m &< n | |
bound by the type signature for: | |
inj :: forall (m :: Nat) (n :: Nat). | |
(m &< n) => | |
SNat m -> SNat n -> Fin n | |
at Implicit.hs:56:1-69 | |
or from: m ~ 'S n1 | |
bound by a pattern with constructor: | |
SS :: forall (n :: Nat). Sing n -> Sing ('S n), | |
in an equation for ‘inj’ | |
at Implicit.hs:58:6-10 | |
or from: n ~ 'S n2 | |
bound by a pattern with constructor: | |
SS :: forall (n :: Nat). Sing n -> Sing ('S n), | |
in an equation for ‘inj’ | |
at Implicit.hs:58:14-18 | |
• In the first argument of ‘FS’, namely ‘(inj n' m')’ | |
In the expression: FS (inj n' m') | |
In an equation for ‘inj’: inj (SS n') (SS m') = FS (inj n' m') | |
| | |
58 | inj (SS n') (SS m') = FS (inj n' m') -- Everything breaks; the proof is uninferrable | |
| ^^^^^^^^^ | |
-} | |
_LTD'' ∷ S m !< S n → m !< n | |
_LTD'' (LTS lt) = lt | |
-- I think this is the real heart of the problem? | |
_LTD' ∷ Dict (S m &< S n) → Dict (m &< n) | |
_LTD' Dict = undefined | |
-- But how would you even use this? | |
_LTD ∷ (S m &< S n) :- (m &< n) | |
_LTD = unmapDict _LTD' | |
-------------------------------------------------------------------------------- | |
-- In case it's useful, here are singleton types and whatnot for `Fin`. (For | |
-- reasons I don't understand, `singletons` can't automatically generate these | |
-- for GADTs like `Fin`. Since everything below works, I guess `singletons` | |
-- usually does more than this, and it's one or more of those other things that | |
-- aren't possible.) | |
data instance Sing (_fn :: Fin n) where | |
SFZ :: Sing FZ | |
SFS :: Sing fn -> Sing (FS fn) | |
type SFin = (Sing :: Fin n -> Type) | |
instance SingI FZ where | |
sing = SFZ | |
instance SingI fn => SingI (FS fn) where | |
sing = SFS (sing :: Sing fn) | |
instance SingKind (Fin n) where | |
type instance Demote (Fin n) = Fin n | |
fromSing SFZ = FZ | |
fromSing (SFS n) = FS (fromSing n) | |
toSing FZ = SomeSing SFZ | |
toSing (FS n) = case toSing n of | |
SomeSing sfn -> SomeSing (SFS sfn) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment